[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 MHonArc.