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,
§3.6).

Hope this helps,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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