如何從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

回答