如何从伊莎贝尔/霍尔生成LaTeX？

Question

如何使用Isabelle/HOL从我的源文件中自动生成LaTeX？

伊莎贝尔/霍尔的tutorial.pdf非常漂亮。我要用LaTeX写一篇论文，里面有很多伊莎贝尔代码。

Answer 1

您应该首先查看现有的文档，然后再返回更具体的问题(如果还存在的话；但我肯定会的；)。

你想要做的就是在伊莎贝尔里做文件准备。第四章首先介绍了伊莎贝尔系统手册的相关理论。(实际上，首先阅读关于Isabelle会话和构建管理的前一章也是个好主意。)

对于一些简洁的表示法，伊莎贝尔文件的LaTeX糖可能也很感兴趣。

其他一些有用的东西，比如从您的伊莎贝尔理论中生成TeX片段，并将它们包含在您的文档中(您可以与其他没有安装伊莎贝尔的人合作)，可以在社区Wiki上找到它们。