Re: [isabelle] Formalizations of Free Groups and Matrix Groups?

Hi Timothy,

> I have a related question.  Looking at src/HOL/Algebra/Group.thy, 
> I see that (for example) the definition of the monoid locale has 
> "fixes G (structure)".  Looking in the documentation, 
> "(structure)" is mentioned only twice in doc/isar-ref.pdf (as far 
> as I can see), and I haven't found it in the other documentation I 
> looked in.  What does it mean?  How would I go about instantiating 
> such a locale?

(structure) is an (outdated) syntax feature.  As far as I understand it
has no relevance for locale interpretation.

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.