如何从Isabelle/HOL生成LaTeX? [英] How do I generate LaTeX from Isabelle/HOL?

问题描述

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

How can I use Isabelle/HOL to automatically generate LaTeX from my source theory files?

Isabelle/HOL的 tutorial.pdf 非常漂亮.我要在LaTeX中写一篇包含很多Isabelle代码的论文.

Isabelle/HOL's tutorial.pdf is very beautiful. I'm going to write a paper in LaTeX with a lot of Isabelle code in it.

推荐答案

您应该首先查看现有文档，然后再提出更具体的问题(如果有的话，不过我敢肯定会;;) ).

You should first have a look at the existing documentation and come back with more specific questions afterwards (if there remain any; but I'm sure there will ;)).

您要执行的操作在Isabelle中称为文档准备.首先要看的是第4章呈现理论 《伊莎贝尔系统手册》 . (实际上，首先阅读有关 Isabelle会话和构建管理的上一章也是一个好主意.)

What you want to do is called document preparation in Isabelle. The first place to look is Chapter 4 Presenting Theories of the Isabelle System Manual. (Actually it is also a good idea to first read the previous chapter on Isabelle sessions and build management.)

对于某些简洁的注释，用于Isabelle文档的LaTeX Sugar 可能也很有趣

For some neat notation also LaTeX Sugar for Isabelle Documents might be of interest.

可以找到其他有用的东西，例如从Isabelle理论生成 TeX片段，并将其包含在文档中(您可以与未安装Isabelle的其他人共同努力). 社区Wiki .

Some other useful things, like generating TeX snippets from your Isabelle theories and including them in your document (which you might collaboratively work on with others that do not have Isabelle installed), can be found on the Community Wiki.

这篇关于如何从Isabelle/HOL生成LaTeX?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！