src/HOL/Algebra/Group.thy
changeset 15076 4b3d280ef06a
parent 14963 d584e32f7d46
child 15696 1da4ce092c0b
     1.1 --- a/src/HOL/Algebra/Group.thy	Thu Jul 22 19:33:12 2004 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Mon Jul 26 15:48:50 2004 +0200
     1.3 @@ -540,7 +540,7 @@
     1.4  
     1.5  
     1.6  text{*Basis for homomorphism proofs: we assume two groups @{term G} and
     1.7 -  @term{H}, with a homomorphism @{term h} between them*}
     1.8 +  @{term H}, with a homomorphism @{term h} between them*}
     1.9  locale group_hom = group G + group H + var h +
    1.10    assumes homh: "h \<in> hom G H"
    1.11    notes hom_mult [simp] = hom_mult [OF homh]
    1.12 @@ -553,7 +553,7 @@
    1.13  lemma (in group_hom) hom_one [simp]:
    1.14    "h \<one> = \<one>\<^bsub>H\<^esub>"
    1.15  proof -
    1.16 -  have "h \<one> \<otimes>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = h \<one> \<otimes>\<^sub>2 h \<one>"
    1.17 +  have "h \<one> \<otimes>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = h \<one> \<otimes>\<^bsub>H\<^esub> h \<one>"
    1.18      by (simp add: hom_mult [symmetric] del: hom_mult)
    1.19    then show ?thesis by (simp del: r_one)
    1.20  qed