--- a/src/ZF/Constructible/L_axioms.thy Sat Oct 10 22:02:23 2015 +0200
+++ b/src/ZF/Constructible/L_axioms.thy Sat Oct 10 22:08:43 2015 +0200
@@ -131,7 +131,7 @@
terms become enormous!\<close>
definition
L_Reflects :: "[i=>o,[i,i]=>o] => prop" ("(3REFLECTS/ [_,/ _])") where
- "REFLECTS[P,Q] == (??Cl. Closed_Unbounded(Cl) &
+ "REFLECTS[P,Q] == (\<Or>Cl. Closed_Unbounded(Cl) &
(\<forall>a. Cl(a) \<longrightarrow> (\<forall>x \<in> Lset(a). P(x) \<longleftrightarrow> Q(a,x))))"
--- a/src/ZF/Constructible/MetaExists.thy Sat Oct 10 22:02:23 2015 +0200
+++ b/src/ZF/Constructible/MetaExists.thy Sat Oct 10 22:08:43 2015 +0200
@@ -6,17 +6,14 @@
theory MetaExists imports Main begin
-text\<open>Allows quantification over any term having sort @{text logic}. Used to
-quantify over classes. Yields a proposition rather than a FOL formula.\<close>
+text\<open>Allows quantification over any term. Used to quantify over classes.
+Yields a proposition rather than a FOL formula.\<close>
definition
- ex :: "(('a::{}) => prop) => prop" (binder "?? " 0) where
- "ex(P) == (!!Q. (!!x. PROP P(x) ==> PROP Q) ==> PROP Q)"
+ ex :: "(('a::{}) \<Rightarrow> prop) \<Rightarrow> prop" (binder "\<Or>" 0) where
+ "ex(P) == (\<And>Q. (\<And>x. PROP P(x) \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q)"
-notation (xsymbols)
- ex (binder "\<Or>" 0)
-
-lemma meta_exI: "PROP P(x) ==> (?? x. PROP P(x))"
+lemma meta_exI: "PROP P(x) ==> (\<Or>x. PROP P(x))"
proof (unfold ex_def)
assume P: "PROP P(x)"
fix Q
@@ -24,7 +21,7 @@
from P show "PROP Q" by (rule PQ)
qed
-lemma meta_exE: "[| ?? x. PROP P(x); !!x. PROP P(x) ==> PROP R |] ==> PROP R"
+lemma meta_exE: "[|\<Or>x. PROP P(x); \<And>x. PROP P(x) ==> PROP R |] ==> PROP R"
proof (unfold ex_def)
assume QPQ: "\<And>Q. (\<And>x. PROP P(x) \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q"
assume PR: "\<And>x. PROP P(x) \<Longrightarrow> PROP R"
--- a/src/ZF/Constructible/Normal.thy Sat Oct 10 22:02:23 2015 +0200
+++ b/src/ZF/Constructible/Normal.thy Sat Oct 10 22:08:43 2015 +0200
@@ -456,12 +456,9 @@
numbers.\<close>
definition
- Aleph :: "i => i" where
+ Aleph :: "i => i" ("\<aleph>_" [90] 90) where
"Aleph(a) == transrec2(a, nat, \<lambda>x r. csucc(r))"
-notation (xsymbols)
- Aleph ("\<aleph>_" [90] 90)
-
lemma Card_Aleph [simp, intro]:
"Ord(a) ==> Card(Aleph(a))"
apply (erule trans_induct3)
--- a/src/ZF/Induct/Comb.thy Sat Oct 10 22:02:23 2015 +0200
+++ b/src/ZF/Induct/Comb.thy Sat Oct 10 22:08:43 2015 +0200
@@ -21,10 +21,7 @@
datatype comb =
K
| S
- | app ("p \<in> comb", "q \<in> comb") (infixl "@@" 90)
-
-notation (xsymbols)
- app (infixl "\<bullet>" 90)
+ | app ("p \<in> comb", "q \<in> comb") (infixl "\<bullet>" 90)
text \<open>
Inductive definition of contractions, @{text "-1->"} and
--- a/src/ZF/Induct/Multiset.thy Sat Oct 10 22:02:23 2015 +0200
+++ b/src/ZF/Induct/Multiset.thy Sat Oct 10 22:08:43 2015 +0200
@@ -75,10 +75,8 @@
syntax
"_MColl" :: "[pttrn, i, o] => i" ("(1{# _ \<in> _./ _#})")
-syntax (xsymbols)
- "_MColl" :: "[pttrn, i, o] => i" ("(1{# _ \<in> _./ _#})")
translations
- "{#x \<in> M. P#}" == "CONST MCollect(M, %x. P)"
+ "{#x \<in> M. P#}" == "CONST MCollect(M, \<lambda>x. P)"
(* multiset orderings *)