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



Hi,

On Sun, 16 May 2010 20:57:27 Florian Haftmann wrote:
> (structure) is an (outdated) syntax feature.  As far as I
> understand it has no relevance for locale interpretation.

Thanks for your reply.  It took me a while to figure out that I 
needed to use \<^bsub>...\<^esub> in a group interpretation.  For 
example, an interpretation of the integers under addition as a 
group might begin:

interpretation group "(|carrier = UNIV, mult = op +, one = 
0::int|)"
proof
  let ?Z = "(|carrier = UNIV, mult = op +, one = 0::int|)"
  fix x y
  show "x ⊗\<^bsub>?Z\<^esub> y ∈ carrier ?Z" by simp

Timothy
<><

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



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