src/HOL/ZF/HOLZF.thy

   by (auto simp add: union_def Sum Upair)
 
 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
   "isFun f == (! x y1 y2. Elem (Opair x y1) f & Elem (Opair x y2) f \<longrightarrow> y1 = y2)"