오래된 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은 가야합니다. 그러나 ML_file사이에begin과 end 명령을 시작/종료해야합니다. 또한, ML_file 호출이 당신은 ML 파일 내부에 사용 아무것도의 정의 (상수, 사실, 정리 컬렉션, simprocs, ...) 당신의 예에서

후 을해야합니다, 그것은 다음과 같아야합니다

theory my_theory 
imports Main 
begin 

lemma my_lemma: ... 
    by ... 

ML_file "my_theory.ML" 

end 

이사벨이 많이 바뀝니다. 당신이 가지고있는 ML 코드는 - 특히 그것이 오래 되었다면 - 아마도 현대 Isabelle 버전과 작동하기 전에 많은 변화가 필요할 것입니다. 그것을 처음부터 다시 쓰는 것이 더 쉬울 수도 있습니다. 이것이 바로 Isabelle 프로젝트를 Archive of Formal Proofs에 넣어야하는 이유입니다.이 프로젝트에서는 개발자가 Isabelle 시스템의 변경 사항을 업데이트합니다. AFP 외부의 이사벨 프로젝트는 수년 내에 부패에 빠질 가능성이 큽니다.