src/HOL/Algebra/Group.thy
 changeset 15763 b901a127ac73 parent 15696 1da4ce092c0b child 16417 9bc16273c2d4
```     1.1 --- a/src/HOL/Algebra/Group.thy	Sun Apr 17 19:40:43 2005 +0200
1.2 +++ b/src/HOL/Algebra/Group.thy	Mon Apr 18 09:25:23 2005 +0200
1.3 @@ -470,8 +470,8 @@
1.4    done
1.5
1.6  text{*This alternative proof of the previous result demonstrates interpret.
1.7 -   It uses @{text Prod.inv_equality} (available after instantiation) instead of
1.8 -   @{text "group.inv_equality [OF DirProd_group]"}. *}
1.9 +   It uses @{text Prod.inv_equality} (available after @{text interpret})
1.10 +   instead of @{text "group.inv_equality [OF DirProd_group]"}. *}
1.11  lemma
1.12    includes group G + group H
1.13    assumes g: "g \<in> carrier G"
1.14 @@ -542,19 +542,8 @@
1.15    @{term H}, with a homomorphism @{term h} between them*}
1.16  locale group_hom = group G + group H + var h +
1.17    assumes homh: "h \<in> hom G H"
1.18 -(*
1.19    notes hom_mult [simp] = hom_mult [OF homh]
1.20      and hom_closed [simp] = hom_closed [OF homh]
1.21 -CB: late binding problem?
1.22 -*)
1.23 -
1.24 -lemma (in group_hom) hom_mult [simp]:
1.25 -  "[| x \<in> carrier G; y \<in> carrier G |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
1.26 -  by (simp add: hom_mult [OF homh])
1.27 -
1.28 -lemma (in group_hom) hom_closed [simp]:
1.29 -  "x \<in> carrier G ==> h x \<in> carrier H"
1.30 -  by (simp add: hom_closed [OF homh])
1.31
1.32  lemma (in group_hom) one_closed [simp]:
1.33    "h \<one> \<in> carrier H"
```