[isabelle] syntax for a type abbreviations
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>?
This archive was generated by a fusion of
Pipermail (Mailman edition) and