latex - 在伊莎贝尔准备文件

Question

我想用isabelle build -D xxx生产 latex .tex从伊莎贝尔文件中取出 .thy文件。
但是 Isabelle 检查了所有理论依赖项，以及所有相关的 .thy必须涉及文件。

有没有可能我随便用一个.thy有语法错误的文件会产生 .tex文件？事实上，我只需要其中的一部分来写一篇论文。

Answer 1

这是否意味着您想根据错误或不完整的形式理论写一篇论文？

Isabelle 文档准备系统旨在发布实际可行的正式理论，并使用漂亮的排版，使其看起来不像“代码”。因此，所有默认值都是用于从格式良好且经过检查的理论生成 LaTeX。

尽管如此，有很多方法可以从系统中获得非官方的 LaTeX 输出。一个非常基本的机制是 latex打印模式。 Isabelle 的各种诊断命令允许在圆括号中指定此类打印模式，例如像这样:

thm (latex) exI exE

或者

print_statement (latex) exI exE

您可以以交互方式执行此操作并将输出复制粘贴到原始 tex 文件中。您需要确保它获得来自 isabelle.sty 的环境的适当环境。文件。