src/HOL/Algebra/Group.thy

 (*
   Title:  HOL/Algebra/Group.thy
-  Id:     $Id$
   Author: Clemens Ballarin, started 4 February 2003
 
 Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
 *)
 

 
 lemma (in subgroup) subgroup_is_group [intro]:
   assumes "group G"
   shows "group (G\<lparr>carrier := H\<rparr>)"
 proof -
-  interpret group [G] by fact
+  interpret group G by fact
   show ?thesis
     apply (rule monoid.group_l_invI)
     apply (unfold_locales) [1]
     apply (auto intro: m_assoc l_inv mem_carrier)
     done

 
 lemma DirProd_monoid:
   assumes "monoid G" and "monoid H"
   shows "monoid (G \<times>\<times> H)"
 proof -
-  interpret G: monoid [G] by fact
-  interpret H: monoid [H] by fact
+  interpret G!: monoid G by fact
+  interpret H!: monoid H by fact
   from assms
   show ?thesis by (unfold monoid_def DirProd_def, auto) 
 qed
 
 
 text{*Does not use the previous result because it's easier just to use auto.*}
 lemma DirProd_group:
   assumes "group G" and "group H"
   shows "group (G \<times>\<times> H)"
 proof -
-  interpret G: group [G] by fact
-  interpret H: group [H] by fact
+  interpret G!: group G by fact
+  interpret H!: group H by fact
   show ?thesis by (rule groupI)
      (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
            simp add: DirProd_def)
 qed
 

   assumes "group G" and "group H"
   assumes g: "g \<in> carrier G"
       and h: "h \<in> carrier H"
   shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
 proof -
-  interpret G: group [G] by fact
-  interpret H: group [H] by fact
-  interpret Prod: group ["G \<times>\<times> H"]
+  interpret G!: group G by fact
+  interpret H!: group H by fact
+  interpret Prod!: group "G \<times>\<times> H"
     by (auto intro: DirProd_group group.intro group.axioms assms)
   show ?thesis by (simp add: Prod.inv_equality g h)
 qed
 
 

 by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def) 
 
 
 text{*Basis for homomorphism proofs: we assume two groups @{term G} and
   @{term H}, with a homomorphism @{term h} between them*}
-locale group_hom = group G + group H + var h +
+locale group_hom = G: group G + H: group H for G (structure) and H (structure) +
+  fixes h
   assumes homh: "h \<in> hom G H"
   notes hom_mult [simp] = hom_mult [OF homh]
     and hom_closed [simp] = hom_closed [OF homh]
 
 lemma (in group_hom) one_closed [simp]: