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
```