[isabelle] syntax for a type abbreviations



Hi,

I have the following type abbreviations:

   types
     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>?

Thanks,
Patrice




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.