isabelle - Isabelle/Isar 中的编码风格约定

Question

TL;DR：Isar 语言是否有任何编码约定？有必要尊重jEdit的折叠策略吗？

---

我的团队正在研究数学的形式化，所以我们的主要目的之一是获得可读的证明。对此进行调查，我们尝试以一种中间事实（和标签，如果有的话）突出的方式对证明进行编码：

from fact1 have
  1: "Foo"
  using Thm1 Thm2 by auto
then have
  2: "Bar = FooBar"
  by simp
also from 1 have
  " ... = BarFoo"
  by blast 

等等。除了有时这会产生“短线”的扩散（顺便说一句，我不知道这是否真的是一个问题），它在某种程度上与 jEdit 折叠策略不兼容；折叠后，前一个代码块如下所示：

from fact1 have
then have
also from 1 have

完全掩盖了论点。以下格式可能更好：

from fact1
have 1: "Foo"
  using Thm1 Thm2 by auto
then 
have 2: "Bar = FooBar"
  by simp
also from 1 
have " ... = BarFoo"
  by blast 

而且，折叠后，

from fact1
have 1: "Foo"
then 
have 2: "Bar = FooBar"
also from 1 
have " ... = BarFoo"

这使得参数的流程变得明确。

无论如何，在我提出 5 个新的格式约定之前，我肯定想知道是否有一些事实上的标准，或者至少是否有人考虑过这一点。