Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Algebra/Group.thy
changeset 61384 9f5145281888
parent 61382 efac889fccbc
child 61565 352c73a689da 
--- a/src/HOL/Algebra/Group.thy	Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Algebra/Group.thy	Sat Oct 10 19:22:05 2015 +0200
@@ -576,7 +576,7 @@
 definition
   hom :: "_ => _ => ('a => 'b) set" where
   "hom G H =
-    {h. h \<in> carrier G -> carrier H &
+    {h. h \<in> carrier G \<rightarrow> carrier H &
       (\<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)}"
 
 lemma (in group) hom_compose:
isabelle