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/ZF/HOLZF.thy
changeset 67443 3abf6a722518
parent 63901 4ce989e962e0
child 67613 ce654b0e6d69 
--- a/src/HOL/ZF/HOLZF.thy	Tue Jan 16 09:12:16 2018 +0100
+++ b/src/HOL/ZF/HOLZF.thy	Tue Jan 16 09:30:00 2018 +0100
@@ -188,7 +188,7 @@
 definition Field :: "ZF \<Rightarrow> ZF" where
   "Field A == union (Domain A) (Range A)"
 
-definition app :: "ZF \<Rightarrow> ZF => ZF" (infixl "\<acute>" 90) \<comment>\<open>function application\<close> where
+definition app :: "ZF \<Rightarrow> ZF => ZF" (infixl "\<acute>" 90) \<comment> \<open>function application\<close> where
   "f \<acute> x == (THE y. Elem (Opair x y) f)"
 
 definition isFun :: "ZF \<Rightarrow> bool" where
isabelle