Ich habe mehrere .thy Dateien in Isabelle heruntergeladen, die (*<*) und (*>*) verwenden. Sie scheinen keine Wirkung zu haben, so weit ich sagen kann, aber sie müssen einen Zweck haben. Weiß jemand, wofür sie gebraucht werden?Was ist (*> *) in Isabelle?
Die Sonderkommentare (*<*) und (*>*) teilen dem Dokumentvorbereitungssystem von Isabelle mit, dass sie den beigefügten Theorietext nicht in die generierten PDF-Dokumente einbezieht. Sie sind die Vorgänger der strukturierteren Tags wie %invisible, die auch steuern, was in den generierten Dokumenten erscheint. Zum Beispiel
lemma %invisible silly: "0 = 0" by simp
und
(*<*)
lemma silly: "0 = 0" by simp
(*>*)
haben in etwa die gleiche Wirkung, nämlich die ganze Lemma und seinen Beweis wird in dem Dokument nicht angezeigt. Tags können jedoch nur an Befehle der obersten Ebene wie definition, lemma, proof, by angehängt werden. Daher können Sie nicht nur Teile eines Befehls wie in
by(simp add: take_map(*<*) drop_map(*>*))
verstecken, die by(simp add: take_map) im PDF ergeben wird, das heißt die drop_map weggelassen.