# HG changeset patch
# User wenzelm
# Date 1491340876 -7200
# Node ID e3fb3036a00ec97d0bd8741665fc5baf651b274a
# Parent  23f36ab9042b1a1c46bfa1f116901d48f7f901b9
allow to load this into "isabelle jedit -l HOL";

diff -r 23f36ab9042b -r e3fb3036a00e src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Tue Apr 04 23:12:08 2017 +0200
+++ b/src/ZF/ZF.thy	Tue Apr 04 23:21:16 2017 +0200
@@ -217,7 +217,7 @@
 definition relation :: "i \<Rightarrow> o"  \<comment> \<open>recognizes sets of pairs\<close>
   where "relation(r) == \<forall>z\<in>r. \<exists>x y. z = \<langle>x,y\<rangle>"
 
-definition function :: "i \<Rightarrow> o"  \<comment> \<open>recognizes functions; can have non-pairs\<close>
+definition "function" :: "i \<Rightarrow> o"  \<comment> \<open>recognizes functions; can have non-pairs\<close>
   where "function(r) == \<forall>x y. \<langle>x,y\<rangle> \<in> r \<longrightarrow> (\<forall>y'. \<langle>x,y'\<rangle> \<in> r \<longrightarrow> y = y')"
 
 definition Image :: "[i, i] \<Rightarrow> i"  (infixl "``" 90)  \<comment> \<open>image\<close>