이사벨 (Isabelle)에 ML 코드를 작성하기 위해 "이사벨 요리 책"을 연구 중입니다.이사벨 (Isabelle)의 ML 프로그래밍 : 내장 함수 및 전술 중 일부를 찾을 수 없음
불행히도 내장 함수를 찾을 수 없으므로 (이름이 변경되었거나 경로 structure.fct를 지정해야하기 때문에) 많은 예제가 작동하지 않습니다. 예를 들어 etac, rtac 및 atac을 사용하는 예제는 더 이상 작동하지 않습니다. 새로운 이름은 무엇이며 어떻게 나 혼자서 찾을 수 있습니까?
Isabelle 요리 책은 항상 매우 비공식적 인 지위를 가지고 있었고, 나는 이제 그것이 심각하게 시대에 뒤 떨어진 것으로 의심 할 것입니다. 거기에 좋은 정보가 있지만 '공식'최신 소스는 이사벨 구현 설명서입니다.
이름이 바뀐 항목의 이름을 찾으려면 NEWS 파일을 살펴 보는 것이 유용 할 수 있습니다. 이 경우 :
* Old tactic shorthands atac, rtac, etac, dtac, ftac have been
discontinued. INCOMPATIBILITY, use regular assume_tac, resolve_tac etc.
instead (with proper context).
~~/src/Pure/tactic.ML에서 찾을 수 있습니다. ML 기능을 찾고 있다면 ~~/src/Pure/ 디렉토리를 검색하면됩니다. jEdit의 하이퍼 검색은 특히 유용합니다.