isabelle - 如何从 Windows 安装中导出 Isabelle 会话？

Question

我有简单的理论文件

theory Max_Of_Two_Integers_Real
  imports (* Main *)
    "../Imperative_HOL" 
    Subarray
    "HOL-Library.Multiset"
    "HOL-Library.Code_Target_Numeral"
    "HOL-Library.Code_Target_Nat"
    "HOL-Library.Code_Abstract_Nat"
begin

definition two_integer_max_case_def :: "nat ⇒ nat ⇒ nat" where
"two_integer_max_case_def a b = (case a > b of True ⇒ a | False ⇒ b)"

definition "example_case_def = two_integer_max_case_def 1 2"

export_code example_case_def checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp

end

我可以看到我的 jEdit 'Plugins - Isabelle - Browse Session information' 我的会话名称是 HOL。所以我试图导出这个会话：

tomr@DESKTOP /cygdrive/c/Homes/Isabelle2021/Isabelle2021
$ isabelle export -O /cygdrive/c/test -x *:**  HOL

一般来说，导出是好的——它包含很多标记*文件，它们可能是 XML 中抽象语法树的先驱。但是没有文件可以归因于我的 Max_Of_Two_Integers_Real。我自己的理论文件中也没有导入任何 HOL_Imperative 文件。

所以 - 导出导出了非常大的会话数据，但我的理论文件和导入的理论文件不在导出的文件中。我做错了什么？如何要求从会话中导出我的理论文件？

我的理论文件非常简单，虽然有错误阻止了代码的生成，但通常我的理论文件是有效的——其中没有公开的证明义务，而且在语法上也是正确的。所以 - 它应该已经被出口了。

标签： isabelle