src/HOL/Algebra/Group.thy
 changeset 29237 e90d9d51106b parent 28823 dcbef866c9e2 child 29240 bb81c3709fb6
```     1.1 --- a/src/HOL/Algebra/Group.thy	Tue Dec 16 15:09:37 2008 +0100
1.2 +++ b/src/HOL/Algebra/Group.thy	Tue Dec 16 21:10:53 2008 +0100
1.3 @@ -1,6 +1,5 @@
1.4  (*
1.5    Title:  HOL/Algebra/Group.thy
1.6 -  Id:     \$Id\$
1.7    Author: Clemens Ballarin, started 4 February 2003
1.8
1.9  Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
1.10 @@ -425,7 +424,7 @@
1.11    assumes "group G"
1.12    shows "group (G\<lparr>carrier := H\<rparr>)"
1.13  proof -
1.14 -  interpret group [G] by fact
1.15 +  interpret group G by fact
1.16    show ?thesis
1.17      apply (rule monoid.group_l_invI)
1.18      apply (unfold_locales) 
1.19 @@ -489,8 +488,8 @@
1.20    assumes "monoid G" and "monoid H"
1.21    shows "monoid (G \<times>\<times> H)"
1.22  proof -
1.23 -  interpret G: monoid [G] by fact
1.24 -  interpret H: monoid [H] by fact
1.25 +  interpret G!: monoid G by fact
1.26 +  interpret H!: monoid H by fact
1.27    from assms
1.28    show ?thesis by (unfold monoid_def DirProd_def, auto)
1.29  qed
1.30 @@ -501,8 +500,8 @@
1.31    assumes "group G" and "group H"
1.32    shows "group (G \<times>\<times> H)"
1.33  proof -
1.34 -  interpret G: group [G] by fact
1.35 -  interpret H: group [H] by fact
1.36 +  interpret G!: group G by fact
1.37 +  interpret H!: group H by fact
1.38    show ?thesis by (rule groupI)
1.39       (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
1.41 @@ -526,9 +525,9 @@
1.42        and h: "h \<in> carrier H"
1.43    shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)"
1.44  proof -
1.45 -  interpret G: group [G] by fact
1.46 -  interpret H: group [H] by fact
1.47 -  interpret Prod: group ["G \<times>\<times> H"]
1.48 +  interpret G!: group G by fact
1.49 +  interpret H!: group H by fact
1.50 +  interpret Prod!: group "G \<times>\<times> H"
1.51      by (auto intro: DirProd_group group.intro group.axioms assms)
1.52    show ?thesis by (simp add: Prod.inv_equality g h)
1.53  qed
1.54 @@ -587,7 +586,8 @@
1.55
1.56  text{*Basis for homomorphism proofs: we assume two groups @{term G} and
1.57    @{term H}, with a homomorphism @{term h} between them*}
1.58 -locale group_hom = group G + group H + var h +
1.59 +locale group_hom = G: group G + H: group H for G (structure) and H (structure) +
1.60 +  fixes h
1.61    assumes homh: "h \<in> hom G H"
1.62    notes hom_mult [simp] = hom_mult [OF homh]
1.63      and hom_closed [simp] = hom_closed [OF homh]
```