Isabelle中的（*> *）是什麼？

Question

我已經下載了幾個.thy文件在伊莎貝爾使用(*<*)和(*>*)。他們似乎沒有影響，據我所知，但他們必須有一個目的。有誰知道他們用於什麼？

Answer 1

特別註釋(*<*)和(*>*)告訴Isabelle的文檔準備系統不要在生成的PDF文檔中包含所附的理論文本。他們是像%invisible這樣的更多結構化標籤的前身，它們也控制生成文檔中出現的內容。例如，

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

和

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

有大致相同的效果，即整個引理及證明文件中不會出現。但是，標籤只能附加到頂層命令，如definition，lemma,proof,by。因此，不能隱藏的命令的像在

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

只是部分將在PDF，即，省略了drop_map收率by(simp add: take_map)。