Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] syntax for a type abbreviations

view this post on Zulip Email Gateway (Aug 18 2022 at 12:38):

From: Patrice Chalin <chalin@encs.concordia.ca>
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

Last updated: May 03 2024 at 12:27 UTC