のような定義済み定数 (再帰関数または定義用) を含む理論ファイルをインポートする場合f、現在の理論ファイルでそのような定数を非表示にするにはどうすればよいですか? fつまり、それが自由変数であることを確認したいのです。インポートしたファイルを変更したくありません。
1 に答える
8
それがまさにhide_constコマンドの目的です。例えば、
hide_const f
定義された定数fを現在のコンテキストから完全に削除します (したがって、アクセスできなくなります)。使用する場合
hide_const (open) f
代わりに、ベース名のみが非表示になりますが (つまり、f)、修飾名 (たとえば、理論で定義されているA.f場合) は引き続き機能します。fA
クラス、タイプ、およびファクトに対して同様のコマンドがあります: hide_class、hide_type、およびhide_fact。Isabelle/Isar Reference Manualの 105 ページも参照してください。
于 2013-04-28T05:05:04.063 に答える