--- a/src/ZF/Constructible/MetaExists.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Constructible/MetaExists.thy Thu Jan 03 21:15:52 2019 +0100
@@ -10,7 +10,7 @@
Yields a proposition rather than a FOL formula.\<close>
definition
- ex :: "(('a::{}) \<Rightarrow> prop) \<Rightarrow> prop" (binder "\<Or>" 0) where
+ ex :: "(('a::{}) \<Rightarrow> prop) \<Rightarrow> prop" (binder \<open>\<Or>\<close> 0) where
"ex(P) == (\<And>Q. (\<And>x. PROP P(x) \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q)"
lemma meta_exI: "PROP P(x) ==> (\<Or>x. PROP P(x))"