旧Isabelle项目使用'uses'导入ml文件我应该如何替换？

Question

我继承老伊莎贝尔项目，并想使其达到最新与伊莎贝尔2016年工作当项目启动时，它往往开始你的文件：

theory my_theory 
imports Main uses "my_theory.ML" 
begin 
lemma my_lemma: ... 
by ... 
end 

的使用关键字似乎并不对存在了，所以我已经试过这更改为：

theory my_theory 
imports Main 
begin 
ML_file "my_theory.ML" 

lemma my_lemma: ... 
by ... 

end 

这不包括文件正确，但我最终可能会或可能不相关，如ML文件中的错误：在一条线上的Undefined fact: "my_lemma"代码与@ {thm my_lemma}。

我的更改是否包含使用ML_file命令的ML文件更正？这是否对我收到的ML错误有影响？

Answer 1

我不熟悉uses关键字;在我开始使用伊莎贝尔之前必须放弃一段时间。

ML_file应该是要走的路;但是，您必须在开始/结束该理论的,begin和end命令之间编写ML_file。此外，ML_file调用必须您的ML文件中使用的任何定义（常量，事实，定理的集合，simprocs，...）

在您的例子后，它应该是这样的：

theory my_theory 
imports Main 
begin 

lemma my_lemma: ... 
    by ... 

ML_file "my_theory.ML" 

end 

请注意，伊莎贝尔改变了很多。任何你有的ML代码 - 尤其是如果它是那么古老的 - 在它与现代伊莎贝尔版本一起工作之前可能需要很多改变。从头开始重写它可能会更容易。这就是为什么Isabelle项目应该被放入Archive of Formal Proofs，在那里他们被更新为开发人员对Isabelle系统的任何改变。法新社之外的任何Isabelle项目都可能在几年内屈服于腐烂。