Re: [isabelle] type_synonym and fixed type arguments in a locale?

Hi Randy,

Am 14.05.2013 um 23:48 schrieb Randy Pollack <rpollack at>:

> In the context of this locale want a type synonym:
> type_synonym 'a atm = "int * 'a"
> This is rejected:
> *** Locally fixed type arguments "'a" in type declaration "atm"

The above looks like a bug. However, there's an easy workaround:

    type_synonym 'b atm = "int * 'b"



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