# HG changeset patch
# User wenzelm
# Date 1444507723 -7200
# Node ID 8673ec68c798ba1fffc92a3cc83fed6dd6447553
# Parent  331be2820f902cd19bac42babe4288ff468e6eb0
tuned syntax -- more symbols;

diff -r 331be2820f90 -r 8673ec68c798 src/ZF/Constructible/L_axioms.thy
--- 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))))"
 
 
diff -r 331be2820f90 -r 8673ec68c798 src/ZF/Constructible/MetaExists.thy
--- 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"
diff -r 331be2820f90 -r 8673ec68c798 src/ZF/Constructible/Normal.thy
--- 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) 
diff -r 331be2820f90 -r 8673ec68c798 src/ZF/Induct/Comb.thy
--- 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
diff -r 331be2820f90 -r 8673ec68c798 src/ZF/Induct/Multiset.thy
--- 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 *)