CODEWITHSUNDEEP
symbolsisabelle
IIM
IIM

Reputation: 533

What is (*>*) in Isabelle?

I have downloaded several .thy files in Isabelle that use (*<*) and (*>*).They seem to have no effect as far as I can tell, but they must have a purpose. Does anyone know what they are used for?

Upvotes: 1

Views: 137

Answers (1)

Andreas Lochbihler
Andreas Lochbihler

Reputation: 5058

The special comments (*<*) and (*>*) tell the document preparation system of Isabelle to not include the enclosed theory text in the generated PDF documents. They are the predecessors of the more structured tags like %invisible, which also control what appears in the generated documents. For example,

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

and

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

have roughly the same effect, namely the whole lemma and its proof will not show up in the document. However, tags can only be attached to top-level commands like definition, lemma, proof, by. Hence, you cannot hide just parts of a command like in

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

which will yield by(simp add: take_map) in the PDF, i.e., the drop_map is omitted.

Upvotes: 3

Related Questions