如何从Isabelle/HOL生成LaTeX？

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

伊莎贝尔/ HOL的tutorial.pdf非常漂亮。我要在LaTeX上写一篇文章，里面有很多Isabelle代码。

2013-10-17 njuguoyi

[Isabelle/HOL]（https://isabelle.in.tum.de/） - 一种正式的数学逻辑和编程语言 - 包含从源文件生成LaTeX的机制。这个问题对Stack Overflow来说非常重要。 – davidg

你应该先看看现有的文档，然后再回来更具体的问题（如果还有的话;但我确定会有;））。

想要做的事情叫做文件准备在伊莎贝尔。首先要看的是第4章介绍理论的 the Isabelle System Manual。（其实这也是第一次阅读伊莎贝尔会议前一章和构建管理一个好主意。）

对于一些巧妙的符号也LaTeX Sugar for Isabelle Documents可能会感兴趣。

其他一些有用的东西，比如从伊莎贝尔理论产生TeX的片段并将它们包括在文档中（您可能协作与其他人没有安装伊莎贝尔上工作），可以在Community Wiki找到。

2013-10-17 08:16:11 chris

谢谢，现在我可以用'isabelle mkroot -d'和'isabelle build -D'来完成这项工作。 – njuguoyi

回答