src/HOL/Algebra/Group.thy
changeset 61384 9f5145281888
parent 61382 efac889fccbc
child 61565 352c73a689da
     1.1 --- a/src/HOL/Algebra/Group.thy	Sat Oct 10 16:40:43 2015 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Sat Oct 10 19:22:05 2015 +0200
     1.3 @@ -576,7 +576,7 @@
     1.4  definition
     1.5    hom :: "_ => _ => ('a => 'b) set" where
     1.6    "hom G H =
     1.7 -    {h. h \<in> carrier G -> carrier H &
     1.8 +    {h. h \<in> carrier G \<rightarrow> carrier H &
     1.9        (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y)}"
    1.10  
    1.11  lemma (in group) hom_compose: