isabelle - 有没有学术论文的伊莎贝尔来源的例子？

我已经完成了 Isabelle 的主要开发的大部分内容，并且想知道如何最好地编写相应的学术论文。

从 Isabelle 的资料来看，我可以对这样的论文产生一些特殊的看法。然而，定理、引理和定义的默认呈现似乎几乎肯定会疏远审稿人。

乳胶糖理论有所帮助，但显然只有当我使用反引号手动重述整个理论时。

是否有支持出版物的伊莎贝尔发展的例子，我可以从这里寻找如何最好地进行的灵感？

标签： isabelleliterate-programming

我过去曾这样做过（对于我的硕士论文），只有一种情况你应该这样做：Isabelle 的文档和 Isabelle 开发的文档（如 AFP）。

有些人这样做（Makarius Wenzel，例如，https: //sketis.net/2019/11 ），类似于“具体语义”。但是，这不是一个很好的解决方案。

不这样做的原因：

即使您的工作基于您的开发图像，编译所需的时间也比使用 pdflatex 长得多。
除非您直接键入 LaTeX 宏，否则您可以做的事情会受到更多限制（在 LaTeX 方面）。如果您直接键入乳胶宏，您将无法再生成 HMTL 输出。所以伊莎贝尔的收获是有限的。
许多会议都希望看到 LaTeX 源代码并且他们不运行 Isabelle，因此无论如何您都必须在某个时候生成 LaTeX（甚至可能会做一些后期制作效果，因为 Isabelle 无法做一些事情）。
你很少想使用 Isabelle 的精确定理（LaTeXsugar 可以提供帮助，但它并不完美）。
如果你现在写论文并发现一个你想在 5 年内改正的错字怎么办？5年后，乳胶仍然可以使用。Isabelle2020 可能不会。
您的所有合著者是否在他们的所有计算机上都使用 Isabelle，包括您的笔记本电脑（如果您正在度假并且需要紧急修复）？
你会经常和伊莎贝尔战斗，例如：

文本“\begin{反例}”

引理 True by auto

文本 " \end{反例} "

不行，因为文字是自己的环境，所以需要后期制作效果。

基本上，使用片段机制从理论中提取 LaTeX，然后使用您最喜欢的 LaTeX 编辑器。