Isabelle中的文檔編寫

Question

我想使用isabelle build -D xxx從Isabelle .thy文件中生成LaTeX .tex文件。 但Isabelle檢查所有理論依賴關係，並且必須涉及所有相關的.thy文件。

是否有可能我隨便用.thy文件有語法錯誤產生.tex文件？事實上，我只需要它的一部分來寫一篇論文。

Answer 1

據我所知，沒有。 LaTeX世代要求文件被成功處理，例如，由於notation (latex)命令，並且由於反引號。

如果你只需要你的文件的一部分，只需從生成的.tex文件中拷貝'n'來粘貼它，或者如果你想要更自動化的東西，看看Generate TeX Snippets wiki頁面。

Answer 2

這是否意味着你想寫一篇基於錯誤或不完整形式理論的論文？

伊莎貝爾文件準備系統的目的是發佈正式的理論，實際工作，與漂亮的印刷術，這樣看起來不像「代碼」。因此，所有的默認設置都是用於從格式良好並經過檢查的理論中生成LaTeX。

儘管如此，還是有很多方法可以從系統中獲得非官方的LaTeX輸出。一個非常基本的機制是latex打印模式。 Isabelle的各種診斷命令允許在圓括號內的這種打印模式規範，例如，像這樣：

thm (latex) exI exE 

或

print_statement (latex) exI exE 

可以交互做到這一點，輸出複製粘貼到您的原始文件TEX。您需要確保它從isabelle.sty文件獲得適當的環境。