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

Question

我已经在Isabelle上完成了一个主要开发的更好的部分，并且想知道如何最好地去写相应的学术论文。

从Isabelle资源中，我可以对这样一篇论文产生一种有点特殊的看法。然而，定理、引理和定义的默认呈现似乎几乎肯定会疏远审查者。

乳糖理论有帮助，但显然只有在我使用反引用手动重申整个理论的情况下。

有没有支持出版物的Isabelle发展的例子，我可以从这些例子中寻找灵感，以便最好地在这里继续下去？

Answer 1

我在过去已经这样做了(对于我的硕士论文)，只有一种情况下您应该这样做: Isabelle的文档和Isabelle开发的文档(如法新社)。

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

不这样做的原因：

编译的时间比使用development.

• Unless要长得多，即使你把你的工作建立在你直接输入

1. 的图像上，你也会受到更多的限制(LaTeX wise)。如果直接输入LaTeX宏，就不能再生成HMTL输出。所以伊莎贝尔的收获是有限的。
2. 许多会议都希望看到LaTeX源代码，但它们不运行伊莎贝尔，所以无论如何你都必须在某个时候生成LaTeX (甚至可能做一些后期制作效果，因为伊莎贝尔不能做一些事情)。
3. 你很少想使用伊莎贝尔的确切定理(LaTeXsugar可以帮助你，但如果你现在写论文，发现5年后你想修复的拼写错误，那就不是LaTeXsugar了？5年后，latex仍然可以工作。Isabelle2020可能不会。
4. 你所有的合著者都在他们的所有电脑上使用伊莎贝尔吗，包括你的笔记本电脑?如果你在度假，有紧急修复要做的话？
5. 和你会经常和伊莎贝尔打架，例如：

text“\begin{反例}”

引理True by auto

text“\end{反例}”

不起作用，因为文本是其自身的环境，因此需要后期制作效果。

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