如何使用Isabelle/HOL从源理论文件中自动生成LaTeX?
Isabelle/HOL tutorial.pdf非常漂亮.我将在LaTeX上写一篇论文,里面有很多Isabelle代码.
您应该首先查看现有文档,然后再回过头来提出更具体的问题(如果还有,但我相信会有;)).
您想要做的是在Isabelle中称为文档准备.看的第一个地方是第4章:呈现理论中 的伊莎贝尔系统手册.(实际上,首先阅读关于Isabelle会话和构建管理的前一章也是一个好主意.)
对于一些简洁的符号,LaTeX Sugar for Isabelle Documents也可能会引起关注.
其他一些有用的东西,比如从Isabelle理论中生成TeX片段并将它们包含在您的文档中(您可能与未安装Isabelle的其他人合作)可以在社区Wiki上找到.
| 归档时间: |
|
| 查看次数: |
1950 次 |
| 最近记录: |