>我在这里发现了类似的问题：(5岁，没有答案( https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-October/msg00120.html，但它是不一样的。
假设我已经证明了经典定理，如"((A->B(/\((~A(->B((->B"。 在伊莎贝尔中是否有可能从本文的第 10 页中提取类似于一个术语：http://www21.in.tum.de/~berghofe/papers/TYPES2002_slides.pdf .
我认为这对于使证明独立于框架很重要。 但我也怀疑它们可能无法获得，因为它们不存在！例如，有一个决策程序，它可以决定命题公式是否是重言式。但在此过程中不会生成显式术语。 从这个意义上说，伊莎贝尔的证明是"诚实的"还是"快速的"？ (我对伊莎贝尔/采埃孚特别感兴趣(
> Isabelle 将所有证明简化为原始推理，但默认情况下不会记录显式证明项，除非您明确要求它(这也会导致明显的性能下降(。即使关闭了证明记录，内核也会检查推理，这会将它们简化为原始推理。这还包括通常产生证明的决策过程，尽管也可以将决策过程集成为不安全的预言机。从这个意义上说，伊莎贝尔是"诚实的"，使用你上面的术语。
完整的证明术语可以通过一些 ML 编程打印和访问，但导出工具尚未开发(截至 2019 年(，因为大多数用户不太关心证明术语。