如何从Isabelle/HOL生成LaTeX?

nju*_*oyi 11 latex isabelle

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

Isabelle/HOL tutorial.pdf非常漂亮.我将在LaTeX上写一篇论文,里面有很多Isabelle代码.

chr*_*ris 6

您应该首先查看现有文档,然后再回过头来提出更具体的问题(如果还有,但我相信会有;)).

您想要做的是在Isabelle中称为文档准备.看的第一个地方是第4章:呈现理论的伊莎贝尔系统手册.(实际上,首先阅读关于Isabelle会话和构建管理的前一章也是一个好主意.)

对于一些简洁的符号,LaTeX Sugar for Isabelle Documents也可能会引起关注.

其他一些有用的东西,比如从Isabelle理论中生成TeX片段并将它们包含在您的文档中(您可能与未安装Isabelle的其他人合作)可以在社区Wiki上找到.