4
f과 같은 정의 된 상수 (재귀 함수 또는 정의의 경우)가있는 이론 파일을 가져올 때 어떻게 현재 이론 파일에서 상수를 숨길 수 있습니까? 즉, f이 무료 변수인지 확인하려고합니다. 가져온 파일을 변경하고 싶지 않습니다.정의 된 상수를 숨기는 방법
A
답변
6
이는 정확히 hide_const 명령의 목적입니다. 예를 들어,
hide_const f
완전히 (가 액세스 할 수 없게 따라서 등) 현재 컨텍스트에서 정의 된 상수 f을 제거합니다. 대신
hide_const (open) f
f), 그러나 정규화 된 이름 (예를 들어,
A.f
f 경우는 이론
A에 정의)은 여전히 작동합니다.
클래스, 유형 및 팩트에 대해 유사한 명령이 있습니다 (hide_class, hide_type 및 hide_fact). 또한 the Isabelle/Isar Reference Manual, 105 페이지를 참조하십시오.