src/ZF/ex/Group.thy
changeset 46820 c656222c4dc1
parent 41524 4d2f9a1c24c7
child 46822 95f1e700b712
     1.1 --- a/src/ZF/ex/Group.thy	Sun Mar 04 23:20:43 2012 +0100
     1.2 +++ b/src/ZF/ex/Group.thy	Tue Mar 06 15:15:49 2012 +0000
     1.3 @@ -412,7 +412,7 @@
     1.4  qed
     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 = G: group G + H: group H
    1.10    for G (structure) and H (structure) and h +
    1.11    assumes homh: "h \<in> hom(G,H)"