如何使用 Isabelle/HOL 从我的源理论文件自动生成 LaTeX？
Isabelle/HOL'stutorial.pdf非常漂亮。我打算用 LaTeX 写一篇论文，里面有很多 Isabelle 代码。
问问题
2698 次
1 回答
7
您应该首先查看现有文档，然后再提出更具体的问题（如果还有；但我相信会有；））。
您要做的就是在 Isabelle 中进行文档准备。首先要看的是第 4 章介绍 Isabelle 系统手册的理论。（实际上，先阅读上一章有关Isabelle 会话和构建管理的内容也是一个好主意。）
对于一些简洁的符号，Isabelle Documents 的 LaTeX Sugar可能也很有趣。
其他一些有用的东西，例如从您的 Isabelle 理论生成TeX 片段并将它们包含在您的文档中（您可以与没有安装 Isabelle 的其他人协作处理），可以在Community Wiki上找到。
于 2013-10-17T08:16:11.603 回答