Re: [isabelle] Type parameters in a locale? Datatypes in a locale?

Hi all,

> Class syntax is declared
> both at the theory level and in the class context.

Not exactly.  Class syntax is *only* declared at the theory level, but
inside the class context occurences of the global class operations on
the type parameter 'a of the class are improved to their local
counterparts.  This allows to use syntax uniformly (c.f. class tutorial,

Hope this helps,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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