# HG changeset patch
# User wenzelm
# Date 1444508084 -7200
# Node ID 6142b282b1646cf22319c7c3e942d0a4b743bfe9
# Parent  8673ec68c798ba1fffc92a3cc83fed6dd6447553
tuned syntax -- more symbols;

diff -r 8673ec68c798 -r 6142b282b164 src/ZF/AC/AC15_WO6.thy
--- a/src/ZF/AC/AC15_WO6.thy	Sat Oct 10 22:08:43 2015 +0200
+++ b/src/ZF/AC/AC15_WO6.thy	Sat Oct 10 22:14:44 2015 +0200
@@ -67,7 +67,7 @@
 lemma lemma4: "[| A \<lesssim> i; Ord(i) |] ==> {P(a). a \<in> A} \<lesssim> i"
 apply (unfold lepoll_def)
 apply (erule exE)
-apply (rule_tac x = "\<lambda>x \<in> RepFun(A,P). LEAST j. \<exists>a\<in>A. x=P(a) & f`a=j" 
+apply (rule_tac x = "\<lambda>x \<in> RepFun(A,P). \<mu> j. \<exists>a\<in>A. x=P(a) & f`a=j" 
        in exI)
 apply (rule_tac d = "%y. P (converse (f) `y) " in lam_injective)
 apply (erule RepFunE)
@@ -148,7 +148,7 @@
 
 lemma AC15_WO6_aux1:
      "\<forall>x \<in> Pow(A)-{0}. f`x\<noteq>0 & f`x \<subseteq> x & f`x \<lesssim> m 
-      ==> (\<Union>i<LEAST x. HH(f,A,x)={A}. HH(f,A,i)) = A"
+      ==> (\<Union>i<\<mu> x. HH(f,A,x)={A}. HH(f,A,i)) = A"
 apply (simp add: Ord_Least [THEN OUN_eq_UN])
 apply (rule equalityI)
 apply (fast dest!: less_Least_subset_x)
@@ -158,7 +158,7 @@
 
 lemma AC15_WO6_aux2:
      "\<forall>x \<in> Pow(A)-{0}. f`x\<noteq>0 & f`x \<subseteq> x & f`x \<lesssim> m 
-      ==> \<forall>x < (LEAST x. HH(f,A,x)={A}). HH(f,A,x) \<lesssim> m"
+      ==> \<forall>x < (\<mu> x. HH(f,A,x)={A}). HH(f,A,x) \<lesssim> m"
 apply (rule oallI)
 apply (drule ltD [THEN less_Least_subset_x])
 apply (frule HH_subset_imp_eq)
@@ -175,8 +175,8 @@
 apply (elim bexE conjE exE)
 apply (rule bexI)
  apply (rule conjI, assumption)
- apply (rule_tac x = "LEAST i. HH (f,A,i) ={A}" in exI)
- apply (rule_tac x = "\<lambda>j \<in> (LEAST i. HH (f,A,i) ={A}) . HH (f,A,j) " in exI)
+ apply (rule_tac x = "\<mu> i. HH (f,A,i) ={A}" in exI)
+ apply (rule_tac x = "\<lambda>j \<in> (\<mu> i. HH (f,A,i) ={A}) . HH (f,A,j) " in exI)
  apply (simp_all add: ltD)
 apply (fast intro!: Ord_Least lam_type [THEN domain_of_fun]
             elim!: less_Least_subset_x AC15_WO6_aux1 AC15_WO6_aux2) 
diff -r 8673ec68c798 -r 6142b282b164 src/ZF/AC/AC16_lemmas.thy
--- a/src/ZF/AC/AC16_lemmas.thy	Sat Oct 10 22:08:43 2015 +0200
+++ b/src/ZF/AC/AC16_lemmas.thy	Sat Oct 10 22:14:44 2015 +0200
@@ -60,7 +60,7 @@
 done
 
 lemma InfCard_Least_in:
-     "[| InfCard(x); y \<subseteq> x; y \<approx> succ(z) |] ==> (LEAST i. i \<in> y) \<in> y"
+     "[| InfCard(x); y \<subseteq> x; y \<approx> succ(z) |] ==> (\<mu> i. i \<in> y) \<in> y"
 apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll, 
                          THEN succ_lepoll_imp_not_empty, THEN not_emptyE])
 apply (fast intro: LeastI 
@@ -73,7 +73,7 @@
       ==> {y \<in> Pow(x). y\<approx>succ(succ(n))} \<lesssim> x*{y \<in> Pow(x). y\<approx>succ(n)}"
 apply (unfold lepoll_def)
 apply (rule_tac x = "\<lambda>y \<in> {y \<in> Pow(x) . y\<approx>succ (succ (n))}. 
-                      <LEAST i. i \<in> y, y-{LEAST i. i \<in> y}>" in exI)
+                      <\<mu> i. i \<in> y, y-{\<mu> i. i \<in> y}>" in exI)
 apply (rule_tac d = "%z. cons (fst(z), snd(z))" in lam_injective)
  apply (blast intro!: Diff_sing_eqpoll intro: InfCard_Least_in)
 apply (simp, blast intro: InfCard_Least_in)
diff -r 8673ec68c798 -r 6142b282b164 src/ZF/AC/AC17_AC1.thy
--- a/src/ZF/AC/AC17_AC1.thy	Sat Oct 10 22:08:43 2015 +0200
+++ b/src/ZF/AC/AC17_AC1.thy	Sat Oct 10 22:14:44 2015 +0200
@@ -55,7 +55,7 @@
 (* *********************************************************************** *)
 
 lemma UN_eq_imp_well_ord:
-     "[| x - (\<Union>j \<in> LEAST i. HH(\<lambda>X \<in> Pow(x)-{0}. {f`X}, x, i) = {x}.  
+     "[| x - (\<Union>j \<in> \<mu> i. HH(\<lambda>X \<in> Pow(x)-{0}. {f`X}, x, i) = {x}.  
         HH(\<lambda>X \<in> Pow(x)-{0}. {f`X}, x, j)) = 0;   
         f \<in> Pow(x)-{0} -> x |]   
         ==> \<exists>r. well_ord(x,r)"
@@ -82,7 +82,7 @@
 lemma AC17_AC1_aux1:
      "[| \<forall>f \<in> Pow(x) - {0} -> x. \<exists>u \<in> Pow(x) - {0}. f`u\<notin>u;   
          \<exists>f \<in> Pow(x)-{0}->x.  
-            x - (\<Union>a \<in> (LEAST i. HH(\<lambda>X \<in> Pow(x)-{0}. {f`X},x,i)={x}).   
+            x - (\<Union>a \<in> (\<mu> i. HH(\<lambda>X \<in> Pow(x)-{0}. {f`X},x,i)={x}).   
             HH(\<lambda>X \<in> Pow(x)-{0}. {f`X},x,a)) = 0 |]  
         ==> P"
 apply (erule bexE)
@@ -117,7 +117,7 @@
 apply (erule not_AC1_imp_ex [THEN exE])
 apply (case_tac 
        "\<exists>f \<in> Pow(x)-{0} -> x. 
-        x - (\<Union>a \<in> (LEAST i. HH (\<lambda>X \<in> Pow (x) -{0}. {f`X},x,i) ={x}) . HH (\<lambda>X \<in> Pow (x) -{0}. {f`X},x,a)) = 0")
+        x - (\<Union>a \<in> (\<mu> i. HH (\<lambda>X \<in> Pow (x) -{0}. {f`X},x,i) ={x}) . HH (\<lambda>X \<in> Pow (x) -{0}. {f`X},x,a)) = 0")
 apply (erule AC17_AC1_aux1, assumption)
 apply (drule AC17_AC1_aux2)
 apply (erule allE)
diff -r 8673ec68c798 -r 6142b282b164 src/ZF/AC/AC_Equiv.thy
--- a/src/ZF/AC/AC_Equiv.thy	Sat Oct 10 22:08:43 2015 +0200
+++ b/src/ZF/AC/AC_Equiv.thy	Sat Oct 10 22:14:44 2015 +0200
@@ -196,7 +196,7 @@
      "[| m \<in> nat; u \<lesssim> m |] ==> domain(u) \<lesssim> m"
 apply (unfold lepoll_def)
 apply (erule exE)
-apply (rule_tac x = "\<lambda>x \<in> domain(u). LEAST i. \<exists>y. <x,y> \<in> u & f`<x,y> = i" 
+apply (rule_tac x = "\<lambda>x \<in> domain(u). \<mu> i. \<exists>y. <x,y> \<in> u & f`<x,y> = i" 
        in exI)
 apply (rule_tac d = "%y. fst (converse(f) ` y) " in lam_injective)
 apply (fast intro: LeastI2 nat_into_Ord [THEN Ord_in_Ord] 
diff -r 8673ec68c798 -r 6142b282b164 src/ZF/AC/Cardinal_aux.thy
--- a/src/ZF/AC/Cardinal_aux.thy	Sat Oct 10 22:08:43 2015 +0200
+++ b/src/ZF/AC/Cardinal_aux.thy	Sat Oct 10 22:14:44 2015 +0200
@@ -79,7 +79,7 @@
 apply (blast intro: eqpoll_refl Un_eqpoll_Inf_Ord eqpoll_imp_lepoll)
 done
 
-lemma Least_in_Ord: "[| P(i); i \<in> j; Ord(j) |] ==> (LEAST i. P(i)) \<in> j"
+lemma Least_in_Ord: "[| P(i); i \<in> j; Ord(j) |] ==> (\<mu> i. P(i)) \<in> j"
 apply (erule Least_le [THEN leE])
 apply (erule Ord_in_Ord, assumption)
 apply (erule ltE)
@@ -100,7 +100,7 @@
 
 lemma UN_sing_lepoll: "Ord(a) ==> (\<Union>x \<in> a. {P(x)}) \<lesssim> a"
 apply (unfold lepoll_def)
-apply (rule_tac x = "\<lambda>z \<in> (\<Union>x \<in> a. {P (x) }) . (LEAST i. P (i) =z) " in exI)
+apply (rule_tac x = "\<lambda>z \<in> (\<Union>x \<in> a. {P (x) }) . (\<mu> i. P (i) =z) " in exI)
 apply (rule_tac d = "%z. P (z) " in lam_injective)
 apply (fast intro!: Least_in_Ord)
 apply (fast intro: LeastI elim!: Ord_in_Ord)
diff -r 8673ec68c798 -r 6142b282b164 src/ZF/AC/DC.thy
--- a/src/ZF/AC/DC.thy	Sat Oct 10 22:08:43 2015 +0200
+++ b/src/ZF/AC/DC.thy	Sat Oct 10 22:14:44 2015 +0200
@@ -10,7 +10,7 @@
 
 lemma RepFun_lepoll: "Ord(a) ==> {P(b). b \<in> a} \<lesssim> a"
 apply (unfold lepoll_def)
-apply (rule_tac x = "\<lambda>z \<in> RepFun (a,P) . LEAST i. z=P (i) " in exI)
+apply (rule_tac x = "\<lambda>z \<in> RepFun (a,P) . \<mu> i. z=P (i) " in exI)
 apply (rule_tac d="%z. P (z)" in lam_injective)
  apply (fast intro!: Least_in_Ord)
 apply (rule sym) 
@@ -20,7 +20,7 @@
 text\<open>Trivial in the presence of AC, but here we need a wellordering of X\<close>
 lemma image_Ord_lepoll: "[| f \<in> X->Y; Ord(X) |] ==> f``X \<lesssim> X"
 apply (unfold lepoll_def)
-apply (rule_tac x = "\<lambda>x \<in> f``X. LEAST y. f`y = x" in exI)
+apply (rule_tac x = "\<lambda>x \<in> f``X. \<mu> y. f`y = x" in exI)
 apply (rule_tac d = "%z. f`z" in lam_injective)
 apply (fast intro!: Least_in_Ord apply_equality, clarify) 
 apply (rule LeastI) 
diff -r 8673ec68c798 -r 6142b282b164 src/ZF/AC/HH.thy
--- a/src/ZF/AC/HH.thy	Sat Oct 10 22:08:43 2015 +0200
+++ b/src/ZF/AC/HH.thy	Sat Oct 10 22:14:44 2015 +0200
@@ -116,11 +116,11 @@
             elim!: Hartog_lepoll_selfE)
 done
 
-lemma HH_Least_eq_x: "HH(f, x, LEAST i. HH(f, x, i) = {x}) = {x}"
+lemma HH_Least_eq_x: "HH(f, x, \<mu> i. HH(f, x, i) = {x}) = {x}"
 by (fast intro!: Ord_Hartog HH_Hartog_is_x LeastI)
 
 lemma less_Least_subset_x:
-     "a \<in> (LEAST i. HH(f,x,i)={x}) ==> HH(f,x,a) \<in> Pow(x)-{0}"
+     "a \<in> (\<mu> i. HH(f,x,i)={x}) ==> HH(f,x,a) \<in> Pow(x)-{0}"
 apply (rule HH_values [THEN disjE], assumption)
 apply (rule less_LeastE)
 apply (erule_tac [2] ltI [OF _ Ord_Least], assumption)
@@ -129,17 +129,17 @@
 subsection\<open>Lemmas used in the proofs of AC1 ==> WO2 and AC17 ==> AC1\<close>
 
 lemma lam_Least_HH_inj_Pow: 
-        "(\<lambda>a \<in> (LEAST i. HH(f,x,i)={x}). HH(f,x,a))   
-         \<in> inj(LEAST i. HH(f,x,i)={x}, Pow(x)-{0})"
+        "(\<lambda>a \<in> (\<mu> i. HH(f,x,i)={x}). HH(f,x,a))   
+         \<in> inj(\<mu> i. HH(f,x,i)={x}, Pow(x)-{0})"
 apply (unfold inj_def, simp)
 apply (fast intro!: lam_type dest: less_Least_subset_x 
             elim!: HH_eq_imp_arg_eq Ord_Least [THEN Ord_in_Ord])
 done
 
 lemma lam_Least_HH_inj:
-     "\<forall>a \<in> (LEAST i. HH(f,x,i)={x}). \<exists>z \<in> x. HH(f,x,a) = {z}   
-      ==> (\<lambda>a \<in> (LEAST i. HH(f,x,i)={x}). HH(f,x,a))   
-          \<in> inj(LEAST i. HH(f,x,i)={x}, {{y}. y \<in> x})"
+     "\<forall>a \<in> (\<mu> i. HH(f,x,i)={x}). \<exists>z \<in> x. HH(f,x,a) = {z}   
+      ==> (\<lambda>a \<in> (\<mu> i. HH(f,x,i)={x}). HH(f,x,a))   
+          \<in> inj(\<mu> i. HH(f,x,i)={x}, {{y}. y \<in> x})"
 by (rule lam_Least_HH_inj_Pow [THEN inj_strengthen_type], simp)
 
 lemma lam_surj_sing: 
@@ -161,7 +161,7 @@
 
 lemma f_subsets_imp_UN_HH_eq_x:
      "\<forall>z \<in> Pow(x)-{0}. f`z \<in> Pow(z)-{0}
-      ==> x - (\<Union>j \<in> (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0"
+      ==> x - (\<Union>j \<in> (\<mu> i. HH(f,x,i)={x}). HH(f,x,j)) = 0"
 apply (case_tac "P \<in> {0}" for P, fast)
 apply (drule Diff_subset [THEN PowI, THEN DiffI])
 apply (drule bspec, assumption) 
@@ -183,7 +183,7 @@
 
 lemma f_sing_imp_HH_sing:
      "[| f \<in> (Pow(x)-{0}) -> {{z}. z \<in> x};   
-         a \<in> (LEAST i. HH(f,x,i)={x}) |] ==> \<exists>z \<in> x. HH(f,x,a) = {z}"
+         a \<in> (\<mu> i. HH(f,x,i)={x}) |] ==> \<exists>z \<in> x. HH(f,x,a) = {z}"
 apply (drule less_Least_subset_x)
 apply (frule HH_subset_imp_eq)
 apply (drule apply_type)
@@ -192,10 +192,10 @@
 done
 
 lemma f_sing_lam_bij: 
-     "[| x - (\<Union>j \<in> (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0;   
+     "[| x - (\<Union>j \<in> (\<mu> i. HH(f,x,i)={x}). HH(f,x,j)) = 0;   
          f \<in> (Pow(x)-{0}) -> {{z}. z \<in> x} |]   
-      ==> (\<lambda>a \<in> (LEAST i. HH(f,x,i)={x}). HH(f,x,a))   
-          \<in> bij(LEAST i. HH(f,x,i)={x}, {{y}. y \<in> x})"
+      ==> (\<lambda>a \<in> (\<mu> i. HH(f,x,i)={x}). HH(f,x,a))   
+          \<in> bij(\<mu> i. HH(f,x,i)={x}, {{y}. y \<in> x})"
 apply (unfold bij_def)
 apply (fast intro!: lam_Least_HH_inj lam_surj_sing f_sing_imp_HH_sing)
 done
@@ -219,13 +219,13 @@
 converse
  (converse(\<lambda>x\<in>x. {x}) O
   Lambda
-   (LEAST i. HH(\<lambda>X\<in>Pow(x) - {0}. {f ` X}, x, i) = {x},
+   (\<mu> i. HH(\<lambda>X\<in>Pow(x) - {0}. {f ` X}, x, i) = {x},
     HH(\<lambda>X\<in>Pow(x) - {0}. {f ` X}, x)))
 Perhaps it could be simplified. *)
 
 lemma bijection:
      "f \<in> (\<Pi> X \<in> Pow(x) - {0}. X) 
-      ==> \<exists>g. g \<in> bij(x, LEAST i. HH(\<lambda>X \<in> Pow(x)-{0}. {f`X}, x, i) = {x})"
+      ==> \<exists>g. g \<in> bij(x, \<mu> i. HH(\<lambda>X \<in> Pow(x)-{0}. {f`X}, x, i) = {x})"
 apply (rule exI) 
 apply (rule bij_Least_HH_x [THEN bij_converse_bij])
 apply (rule f_subsets_imp_UN_HH_eq_x)
diff -r 8673ec68c798 -r 6142b282b164 src/ZF/AC/Hartog.thy
--- a/src/ZF/AC/Hartog.thy	Sat Oct 10 22:08:43 2015 +0200
+++ b/src/ZF/AC/Hartog.thy	Sat Oct 10 22:14:44 2015 +0200
@@ -10,7 +10,7 @@
 
 definition
   Hartog :: "i => i"  where
-   "Hartog(X) == LEAST i. ~ i \<lesssim> X"
+   "Hartog(X) == \<mu> i. ~ i \<lesssim> X"
 
 lemma Ords_in_set: "\<forall>a. Ord(a) \<longrightarrow> a \<in> X ==> P"
 apply (rule_tac X = "{y \<in> X. Ord (y) }" in ON_class [elim_format])
diff -r 8673ec68c798 -r 6142b282b164 src/ZF/AC/WO2_AC16.thy
--- a/src/ZF/AC/WO2_AC16.thy	Sat Oct 10 22:08:43 2015 +0200
+++ b/src/ZF/AC/WO2_AC16.thy	Sat Oct 10 22:14:44 2015 +0200
@@ -22,7 +22,7 @@
     "recfunAC16(f,h,i,a) == 
          transrec2(i, 0, 
               %g r. if (\<exists>y \<in> r. h`g \<subseteq> y) then r
-                    else r \<union> {f`(LEAST i. h`g \<subseteq> f`i & 
+                    else r \<union> {f`(\<mu> i. h`g \<subseteq> f`i & 
                          (\<forall>b<a. (h`b \<subseteq> f`i \<longrightarrow> (\<forall>t \<in> r. ~ h`b \<subseteq> t))))})"
 
 (* ********************************************************************** *)
@@ -36,7 +36,7 @@
      "recfunAC16(f,h,succ(i),a) =   
       (if (\<exists>y \<in> recfunAC16(f,h,i,a). h ` i \<subseteq> y) then recfunAC16(f,h,i,a)  
        else recfunAC16(f,h,i,a) \<union>  
-            {f ` (LEAST j. h ` i \<subseteq> f ` j &   
+            {f ` (\<mu> j. h ` i \<subseteq> f ` j &   
              (\<forall>b<a. (h`b \<subseteq> f`j   
               \<longrightarrow> (\<forall>t \<in> recfunAC16(f,h,i,a). ~ h`b \<subseteq> t))))})"
 apply (simp add: recfunAC16_def)
@@ -232,11 +232,11 @@
 
 lemma in_Least_Diff:
      "[| z \<in> F(x); Ord(x) |]   
-      ==> z \<in> F(LEAST i. z \<in> F(i)) - (\<Union>j<(LEAST i. z \<in> F(i)). F(j))"
+      ==> z \<in> F(\<mu> i. z \<in> F(i)) - (\<Union>j<(\<mu> i. z \<in> F(i)). F(j))"
 by (fast elim: less_LeastE elim!: LeastI)
 
 lemma Least_eq_imp_ex:
-     "[| (LEAST i. w \<in> F(i)) = (LEAST i. z \<in> F(i));   
+     "[| (\<mu> i. w \<in> F(i)) = (\<mu> i. z \<in> F(i));   
          w \<in> (\<Union>i<a. F(i)); z \<in> (\<Union>i<a. F(i)) |]   
       ==> \<exists>b<a. w \<in> (F(b) - (\<Union>c<b. F(c))) & z \<in> (F(b) - (\<Union>c<b. F(c)))"
 apply (elim OUN_E)
@@ -255,7 +255,7 @@
      "[| \<forall>i<a. F(i)-(\<Union>j<i. F(j)) \<lesssim> 1; Limit(a) |]   
       ==> (\<Union>x<a. F(x)) \<lesssim> a"
 apply (rule lepoll_def [THEN def_imp_iff [THEN iffD2]])
-apply (rule_tac x = "\<lambda>z \<in> (\<Union>x<a. F (x)). LEAST i. z \<in> F (i) " in exI)
+apply (rule_tac x = "\<lambda>z \<in> (\<Union>x<a. F (x)). \<mu> i. z \<in> F (i) " in exI)
 apply (unfold inj_def)
 apply (rule CollectI)
 apply (rule lam_type)
diff -r 8673ec68c798 -r 6142b282b164 src/ZF/AC/WO6_WO1.thy
--- a/src/ZF/AC/WO6_WO1.thy	Sat Oct 10 22:08:43 2015 +0200
+++ b/src/ZF/AC/WO6_WO1.thy	Sat Oct 10 22:14:44 2015 +0200
@@ -29,9 +29,9 @@
 definition
   vv1 :: "[i, i, i] => i"  where
      "vv1(f,m,b) ==                                                
-           let g = LEAST g. (\<exists>d. Ord(d) & (domain(uu(f,b,g,d)) \<noteq> 0 & 
+           let g = \<mu> g. (\<exists>d. Ord(d) & (domain(uu(f,b,g,d)) \<noteq> 0 & 
                                  domain(uu(f,b,g,d)) \<lesssim> m));      
-               d = LEAST d. domain(uu(f,b,g,d)) \<noteq> 0 &                  
+               d = \<mu> d. domain(uu(f,b,g,d)) \<noteq> 0 &                  
                             domain(uu(f,b,g,d)) \<lesssim> m         
            in  if f`b \<noteq> 0 then domain(uu(f,b,g,d)) else 0"
 
@@ -48,7 +48,7 @@
 definition
   vv2 :: "[i, i, i, i] => i"  where
      "vv2(f,b,g,s) ==   
-           if f`g \<noteq> 0 then {uu(f, b, g, LEAST d. uu(f,b,g,d) \<noteq> 0)`s} else 0"
+           if f`g \<noteq> 0 then {uu(f, b, g, \<mu> d. uu(f,b,g,d) \<noteq> 0)`s} else 0"
 
 definition
   ww2 :: "[i, i, i, i] => i"  where
@@ -210,10 +210,10 @@
 (* ********************************************************************** *)
 lemma nested_LeastI:
      "[| P(a, b);  Ord(a);  Ord(b);   
-         Least_a = (LEAST a. \<exists>x. Ord(x) & P(a, x)) |]   
-      ==> P(Least_a, LEAST b. P(Least_a, b))"
+         Least_a = (\<mu> a. \<exists>x. Ord(x) & P(a, x)) |]   
+      ==> P(Least_a, \<mu> b. P(Least_a, b))"
 apply (erule ssubst)
-apply (rule_tac Q = "%z. P (z, LEAST b. P (z, b))" in LeastI2)
+apply (rule_tac Q = "%z. P (z, \<mu> b. P (z, b))" in LeastI2)
 apply (fast elim!: LeastI)+
 done
 
@@ -260,7 +260,7 @@
 
 lemma uu_not_empty:
      "[| b<a; g<a; f`b\<noteq>0; f`g\<noteq>0;  y*y \<subseteq> y; (\<Union>b<a. f`b)=y |]   
-      ==> uu(f,b,g,LEAST d. (uu(f,b,g,d) \<noteq> 0)) \<noteq> 0"
+      ==> uu(f,b,g,\<mu> d. (uu(f,b,g,d) \<noteq> 0)) \<noteq> 0"
 apply (drule ex_d_uu_not_empty, assumption+)
 apply (fast elim!: LeastI lt_Ord)
 done
@@ -270,7 +270,7 @@
 
 lemma Least_uu_not_empty_lt_a:
      "[| b<a; g<a; f`b\<noteq>0; f`g\<noteq>0; y*y \<subseteq> y; (\<Union>b<a. f`b)=y |]   
-      ==> (LEAST d. uu(f,b,g,d) \<noteq> 0) < a"
+      ==> (\<mu> d. uu(f,b,g,d) \<noteq> 0) < a"
 apply (erule ex_d_uu_not_empty [THEN oexE], assumption+)
 apply (blast intro: Least_le [THEN lt_trans1] lt_Ord)
 done
@@ -298,7 +298,7 @@
           \<forall>b<a. f`b \<lesssim> succ(m);  y*y \<subseteq> y;                        
           (\<Union>b<a. f`b)=y;  b<a;  g<a;  d<a;                             
           f`b\<noteq>0;  f`g\<noteq>0;  m \<in> nat;  s \<in> f`b |] 
-      ==> uu(f, b, g, LEAST d. uu(f,b,g,d)\<noteq>0) \<in> f`b -> f`g"
+      ==> uu(f, b, g, \<mu> d. uu(f,b,g,d)\<noteq>0) \<in> f`b -> f`g"
 apply (drule_tac x2=g in ospec [THEN ospec, THEN mp])
    apply (rule_tac [3] not_empty_rel_imp_domain [OF uu_subset1 uu_not_empty])
         apply (rule_tac [2] Least_uu_not_empty_lt_a, assumption+)
@@ -466,7 +466,7 @@
 
 lemma lemma2:
      "[| (\<Union>b<a. f`b)=y; x \<in> y; \<forall>b<a. f`b \<lesssim> 1; Ord(a) |]   
-      ==> f` (LEAST i. f`i = {x}) = {x}"
+      ==> f` (\<mu> i. f`i = {x}) = {x}"
 apply (drule lemma1, assumption+)
 apply (fast elim!: lt_Ord intro: LeastI)
 done
@@ -475,7 +475,7 @@
 apply (unfold NN_def)
 apply (elim CollectE exE conjE)
 apply (rule_tac x = a in exI)
-apply (rule_tac x = "\<lambda>x \<in> y. LEAST i. f`i = {x}" in exI)
+apply (rule_tac x = "\<lambda>x \<in> y. \<mu> i. f`i = {x}" in exI)
 apply (rule conjI, assumption)
 apply (rule_tac d = "%i. THE x. x \<in> f`i" in lam_injective)
 apply (drule lemma1, assumption+)
diff -r 8673ec68c798 -r 6142b282b164 src/ZF/Arith.thy
--- a/src/ZF/Arith.thy	Sat Oct 10 22:08:43 2015 +0200
+++ b/src/ZF/Arith.thy	Sat Oct 10 22:14:44 2015 +0200
@@ -72,9 +72,6 @@
   mod  :: "[i,i]=>i"                    (infixl "mod" 70)  where
     "m mod n == raw_mod (natify(m), natify(n))"
 
-notation (xsymbols)
-  mult  (infixr "#\<times>" 70)
-
 declare rec_type [simp]
         nat_0_le [simp]
 
diff -r 8673ec68c798 -r 6142b282b164 src/ZF/Cardinal.thy
--- a/src/ZF/Cardinal.thy	Sat Oct 10 22:08:43 2015 +0200
+++ b/src/ZF/Cardinal.thy	Sat Oct 10 22:14:44 2015 +0200
@@ -9,39 +9,33 @@
 
 definition
   (*least ordinal operator*)
-   Least    :: "(i=>o) => i"    (binder "LEAST " 10)  where
+   Least    :: "(i=>o) => i"    (binder "\<mu> " 10)  where
      "Least(P) == THE i. Ord(i) & P(i) & (\<forall>j. j<i \<longrightarrow> ~P(j))"
 
 definition
-  eqpoll   :: "[i,i] => o"     (infixl "eqpoll" 50)  where
-    "A eqpoll B == \<exists>f. f \<in> bij(A,B)"
+  eqpoll   :: "[i,i] => o"     (infixl "\<approx>" 50)  where
+    "A \<approx> B == \<exists>f. f \<in> bij(A,B)"
 
 definition
-  lepoll   :: "[i,i] => o"     (infixl "lepoll" 50)  where
-    "A lepoll B == \<exists>f. f \<in> inj(A,B)"
+  lepoll   :: "[i,i] => o"     (infixl "\<lesssim>" 50)  where
+    "A \<lesssim> B == \<exists>f. f \<in> inj(A,B)"
 
 definition
-  lesspoll :: "[i,i] => o"     (infixl "lesspoll" 50)  where
-    "A lesspoll B == A lepoll B & ~(A eqpoll B)"
+  lesspoll :: "[i,i] => o"     (infixl "\<prec>" 50)  where
+    "A \<prec> B == A \<lesssim> B & ~(A \<approx> B)"
 
 definition
   cardinal :: "i=>i"           ("|_|")  where
-    "|A| == (LEAST i. i eqpoll A)"
+    "|A| == (\<mu> i. i \<approx> A)"
 
 definition
   Finite   :: "i=>o"  where
-    "Finite(A) == \<exists>n\<in>nat. A eqpoll n"
+    "Finite(A) == \<exists>n\<in>nat. A \<approx> n"
 
 definition
   Card     :: "i=>o"  where
     "Card(i) == (i = |i|)"
 
-notation (xsymbols)
-  eqpoll    (infixl "\<approx>" 50) and
-  lepoll    (infixl "\<lesssim>" 50) and
-  lesspoll  (infixl "\<prec>" 50) and
-  Least     (binder "\<mu>" 10)
-
 
 subsection\<open>The Schroeder-Bernstein Theorem\<close>
 text\<open>See Davey and Priestly, page 106\<close>
@@ -89,7 +83,7 @@
 apply (erule exI)
 done
 
-(*A eqpoll A*)
+(*A \<approx> A*)
 lemmas eqpoll_refl = id_bij [THEN bij_imp_eqpoll, simp]
 
 lemma eqpoll_sym: "X \<approx> Y ==> Y \<approx> X"
@@ -160,7 +154,7 @@
 apply (blast intro: inj_disjoint_Un)
 done
 
-(*A eqpoll 0 ==> A=0*)
+(*A \<approx> 0 ==> A=0*)
 lemmas eqpoll_0_is_0 = eqpoll_imp_lepoll [THEN lepoll_0_is_0]
 
 lemma eqpoll_0_iff: "A \<approx> 0 \<longleftrightarrow> A=0"
@@ -239,7 +233,7 @@
   by (blast intro: eqpoll_imp_lepoll lesspoll_trans2)
 
 
-(** LEAST -- the least number operator [from HOL/Univ.ML] **)
+(** \<mu> -- the least number operator [from HOL/Univ.ML] **)
 
 lemma Least_equality:
     "[| P(i);  Ord(i);  !!x. x<i ==> ~P(x) |] ==> (\<mu> x. P(x)) = i"
@@ -296,7 +290,7 @@
   thus ?thesis using P .
 qed
 
-(*LEAST really is the smallest*)
+(*\<mu> really is the smallest*)
 lemma less_LeastE: "[| P(i);  i < (\<mu> x. P(x)) |] ==> Q"
 apply (rule Least_le [THEN [2] lt_trans2, THEN lt_irrefl], assumption+)
 apply (simp add: lt_Ord)
@@ -307,7 +301,7 @@
     "[| P(i);  Ord(i);  !!j. P(j) ==> Q(j) |] ==> Q(\<mu> j. P(j))"
 by (blast intro: LeastI )
 
-(*If there is no such P then LEAST is vacuously 0*)
+(*If there is no such P then \<mu> is vacuously 0*)
 lemma Least_0:
     "[| ~ (\<exists>i. Ord(i) & P(i)) |] ==> (\<mu> x. P(x)) = 0"
 apply (unfold Least_def)
@@ -636,7 +630,7 @@
 done
 
 
-(** lepoll, \<prec> and natural numbers **)
+(** \<lesssim>, \<prec> and natural numbers **)
 
 lemma lepoll_succ: "i \<lesssim> succ(i)"
   by (blast intro: subset_imp_lepoll)
diff -r 8673ec68c798 -r 6142b282b164 src/ZF/CardinalArith.thy
--- a/src/ZF/CardinalArith.thy	Sat Oct 10 22:08:43 2015 +0200
+++ b/src/ZF/CardinalArith.thy	Sat Oct 10 22:14:44 2015 +0200
@@ -37,7 +37,7 @@
   csucc         :: "i=>i"  where
     --\<open>needed because @{term "jump_cardinal(K)"} might not be the successor
         of @{term K}\<close>
-    "csucc(K) == LEAST L. Card(L) & K<L"
+    "csucc(K) == \<mu> L. Card(L) & K<L"
 
 notation (xsymbols)
   cadd  (infixl "\<oplus>" 65) and
diff -r 8673ec68c798 -r 6142b282b164 src/ZF/Cardinal_AC.thy
--- a/src/ZF/Cardinal_AC.thy	Sat Oct 10 22:08:43 2015 +0200
+++ b/src/ZF/Cardinal_AC.thy	Sat Oct 10 22:14:44 2015 +0200
@@ -152,16 +152,16 @@
     assume z: "z \<in> (\<Union>i\<in>K. X(i))"
     then obtain i where i: "i \<in> K" "Ord(i)" "z \<in> X(i)"
       by (blast intro: Ord_in_Ord [of K]) 
-    hence "(LEAST i. z \<in> X(i)) \<le> i" by (fast intro: Least_le) 
-    hence "(LEAST i. z \<in> X(i)) < K" by (best intro: lt_trans1 ltI i) 
-    hence "(LEAST i. z \<in> X(i)) \<in> K" and "z \<in> X(LEAST i. z \<in> X(i))"  
+    hence "(\<mu> i. z \<in> X(i)) \<le> i" by (fast intro: Least_le) 
+    hence "(\<mu> i. z \<in> X(i)) < K" by (best intro: lt_trans1 ltI i) 
+    hence "(\<mu> i. z \<in> X(i)) \<in> K" and "z \<in> X(\<mu> i. z \<in> X(i))"  
       by (auto intro: LeastI ltD i) 
   } note mems = this
   have "(\<Union>i\<in>K. X(i)) \<lesssim> K \<times> K" 
     proof (unfold lepoll_def)
       show "\<exists>f. f \<in> inj(\<Union>RepFun(K, X), K \<times> K)"
         apply (rule exI) 
-        apply (rule_tac c = "%z. \<langle>LEAST i. z \<in> X(i), f ` (LEAST i. z \<in> X(i)) ` z\<rangle>"
+        apply (rule_tac c = "%z. \<langle>\<mu> i. z \<in> X(i), f ` (\<mu> i. z \<in> X(i)) ` z\<rangle>"
                     and d = "%\<langle>i,j\<rangle>. converse (f`i) ` j" in lam_injective) 
         apply (force intro: f inj_is_fun mems apply_type Perm.left_inverse)+
         done