[isabelle] changing the printed syntax for "Some x" (was Re: syntax for a type abbreviations)
On a related note: how can I get "Some x" to display as, say, "[x]"?
Patrice Chalin wrote:
I have the following type abbreviations:
ValOrUndef = "Val option"
"Val\<^isub>\<bottom>" = ValOrUndef
(the above actually parses fine). But then I cannot use
Val\<^isub>\<bottom> in places where a type is expected because a
syntax error is reported. Is there any way I can get ValOrUndef to be
printed (in PDF versions of the theory) as Val\<^isub>\<bottom>?
Patrice Chalin, Eng., Software Engineering UGP Director, Associate Prof.
Dependable Software Research Group, CSE Department, Concordia University
Room EV3.215, Phone +1-514-848-2424 x3004. www.encs.concordia.ca/~chalin
This archive was generated by a fusion of
Pipermail (Mailman edition) and