--- a/src/HOL/Algebra/Group.thy Tue Dec 16 15:09:37 2008 +0100
+++ b/src/HOL/Algebra/Group.thy Tue Dec 16 21:10:53 2008 +0100
@@ -1,6 +1,5 @@
(*
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.
@@ -425,7 +424,7 @@
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]
@@ -489,8 +488,8 @@
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
@@ -501,8 +500,8 @@
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)
@@ -526,9 +525,9 @@
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
@@ -587,7 +586,8 @@
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]