如何从Isabelle/HOL生成LaTeX？

Question

12

我该如何使用Isabelle/HOL从源理论文件自动生成LaTeX?

Isabelle/HOL的tutorial.pdf非常漂亮。我将在LaTeX中写一篇包含大量Isabelle代码的论文。

- njuguoyi

10

Isabelle/HOL是一种正式的数学逻辑和编程语言，它包含从源文件生成LaTeX的机制。这个问题非常适合在Stack Overflow上讨论。 - davidg

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- chris · Accepted Answer

首先，你应该查看现有的文档，并在之后提出更具体的问题（如果还有的话；但我确信会有的;)).

你想要做的是在Isabelle中进行文档准备。首先要看的地方是Isabelle系统手册的第4章呈现理论。（实际上，最好先阅读关于Isabelle会话和构建管理的前一章。）

对于一些漂亮的符号表示，也许Isabelle文档的LaTeX Sugar也会很有兴趣。

其他一些有用的东西，如从Isabelle理论生成TeX片段，并将其包含在您的文档中（您可能与其他没有安装Isabelle的人协作工作），可以在社区Wiki上找到。