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,
	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.