イザベルでは（*> *）とは何ですか？

Question

イザベルで.thyのファイルをいくつかダウンロードしました。そのファイルは(*<*)と(*>*)です。私の言う限りでは効果がないようですが、目的があるはずです。誰が彼らのために使われているか知っていますか？

Answer 1

特別なコメント(*<*)と(*>*)は、生成されたPDF文書に囲まれた理論テキストを含まないようにIsabelleの文書作成システムに指示します。それらは%invisibleのようなより構造化されたタグの前身であり、生成された文書に現れるものも制御します。例えば、

lemma %invisible silly: "0 = 0" by simp 

と

(*<*) 
lemma silly: "0 = 0" by simp 
(*>*) 

は、ドキュメントに表示されませんほぼ同じ効果、すなわち全体の補題とその証拠を持っています。ただし、タグは、 definition, lemma, proof, byのような最上位コマンドにのみアタッチすることができます。したがって、あなたがPDFで by(simp add: take_map)が得られます

by(simp add: take_map(*<*) drop_map(*>*)) 

のようにコマンドのほんの一部を隠すことができない、すなわち、drop_mapが省略されています。