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/BNF_Least_Fixpoint.thy
changeset 67091 1393c2340eec
parent 66290 88714f2e40e8
child 69605 a96320074298 
--- a/src/HOL/BNF_Least_Fixpoint.thy	Sun Nov 26 13:19:52 2017 +0100
+++ b/src/HOL/BNF_Least_Fixpoint.thy	Sun Nov 26 21:08:32 2017 +0100
@@ -54,7 +54,7 @@
   unfolding bij_betw_def inj_on_def by blast
 
 lemma surj_fun_eq:
-  assumes surj_on: "f ` X = UNIV" and eq_on: "\<forall>x \<in> X. (g1 o f) x = (g2 o f) x"
+  assumes surj_on: "f ` X = UNIV" and eq_on: "\<forall>x \<in> X. (g1 \<circ> f) x = (g2 \<circ> f) x"
   shows "g1 = g2"
 proof (rule ext)
   fix y
isabelle