我想用来从 Isabelle文件isabelle build -D xxx中生成 LaTeX文件。但是Isabelle检查了所有的理论依赖，所有的相关文件都必须涉及。.tex.thy.thy
是否有可能我随便使用.thy有语法错误的文件来生成.tex文件？事实上，我只需要其中的一部分来写一篇论文。
问问题
579 次
2 回答
4
这是否意味着你想写一篇基于错误或不完整的形式理论的论文？
Isabelle 文档准备系统旨在发布实际可行的正式理论，并带有漂亮的排版，因此看起来不像“代码”。因此，所有默认值都是用于从格式良好且经过检验的理论生成 LaTeX。
尽管如此，有很多方法可以从系统中获取非官方的 LaTeX 输出。一个非常基本的机制是latex打印模式。Isabelle 的各种诊断命令允许在圆括号中指定此类打印模式，例如：
thm (latex) exI exE
或者
print_statement (latex) exI exE
您可以交互地执行此操作并将输出复制粘贴到您的原始 tex 文件中。isabelle.sty您需要确保它从文件中获得适当的环境。
于 2014-03-14T20:46:47.217 回答
3
据我所知，没有。LaTeX 生成需要成功处理文件，例如由于notation (latex)命令和反引号。
如果您只需要文件的一部分，只需从生成的.tex文件中复制并粘贴它，或者，如果您想要更自动化的东西，请查看Generate TeX Snippets wiki 页面。
于 2013-10-18T17:00:07.483 回答