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



On Sun, 09 May 2010 04:40:41 Brian Huffman wrote:
> Indeed, the Isabelle libraries contain a lot of more concrete
> mathematical constructions, but they are spread over several
> different places, and generally nobody has connected them up
> with HOL/Algebra to show that they are instances of the more
> abstract notions.

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?

Tim
<><

Attachment: signature.asc
Description: This is a digitally signed message part.



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