[isabelle] Syntax translation for types



Hello,

I would like to have Isabelle print types using the type abbreviations I have introduced with "types". To that end, I have come across translations for types that work reasonably well if type variables occur only once. However, I fail to make it work for type abbreviation like this:

types 'a my_type = "('a list × int × 'a list)"

translations
  "my_type a" <= (type) "a list × int × a list"

Isabelle complains that variable a occurs twice in "a list × int × a list". How can I set up an appropriate print translation for such a type abbreviation? Do I need to write an ML translation function? If so, how can I find out how to do that? Or is there any better support other than translations (similar to abbreviation for constants)?

Regards,
Andreas





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