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"