舊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項目都可能在幾年內屈服於腐爛。