diff -r 0c18df79b1c8 -r a642599ffdea src/ZF/AC/DC.thy
--- a/src/ZF/AC/DC.thy	Tue Sep 27 17:03:23 2022 +0100
+++ b/src/ZF/AC/DC.thy	Tue Sep 27 17:46:52 2022 +0100
@@ -11,7 +11,7 @@
 lemma RepFun_lepoll: "Ord(a) \<Longrightarrow> {P(b). b \<in> a} \<lesssim> a"
 apply (unfold lepoll_def)
 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 (rule_tac d="\<lambda>z. P (z)" in lam_injective)
  apply (fast intro!: Least_in_Ord)
 apply (rule sym) 
 apply (fast intro: LeastI Ord_in_Ord) 
@@ -21,7 +21,7 @@
 lemma image_Ord_lepoll: "\<lbrakk>f \<in> X->Y; Ord(X)\<rbrakk> \<Longrightarrow> f``X \<lesssim> X"
 apply (unfold lepoll_def)
 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 (rule_tac d = "\<lambda>z. f`z" in lam_injective)
 apply (fast intro!: Least_in_Ord apply_equality, clarify) 
 apply (rule LeastI) 
  apply (erule apply_equality, assumption+) 
@@ -29,35 +29,35 @@
 done
 
 lemma range_subset_domain: 
-      "\<lbrakk>R \<subseteq> X*X;   \<And>g. g \<in> X \<Longrightarrow> \<exists>u. <g,u> \<in> R\<rbrakk> 
+      "\<lbrakk>R \<subseteq> X*X;   \<And>g. g \<in> X \<Longrightarrow> \<exists>u. \<langle>g,u\<rangle> \<in> R\<rbrakk> 
        \<Longrightarrow> range(R) \<subseteq> domain(R)"
 by blast 
 
-lemma cons_fun_type: "g \<in> n->X \<Longrightarrow> cons(<n,x>, g) \<in> succ(n) -> cons(x, X)"
+lemma cons_fun_type: "g \<in> n->X \<Longrightarrow> cons(\<langle>n,x\<rangle>, g) \<in> succ(n) -> cons(x, X)"
 apply (unfold succ_def)
 apply (fast intro!: fun_extend elim!: mem_irrefl)
 done
 
 lemma cons_fun_type2:
-     "\<lbrakk>g \<in> n->X; x \<in> X\<rbrakk> \<Longrightarrow> cons(<n,x>, g) \<in> succ(n) -> X"
+     "\<lbrakk>g \<in> n->X; x \<in> X\<rbrakk> \<Longrightarrow> cons(\<langle>n,x\<rangle>, g) \<in> succ(n) -> X"
 by (erule cons_absorb [THEN subst], erule cons_fun_type)
 
-lemma cons_image_n: "n \<in> nat \<Longrightarrow> cons(<n,x>, g)``n = g``n"
+lemma cons_image_n: "n \<in> nat \<Longrightarrow> cons(\<langle>n,x\<rangle>, g)``n = g``n"
 by (fast elim!: mem_irrefl)
 
-lemma cons_val_n: "g \<in> n->X \<Longrightarrow> cons(<n,x>, g)`n = x"
+lemma cons_val_n: "g \<in> n->X \<Longrightarrow> cons(\<langle>n,x\<rangle>, g)`n = x"
 by (fast intro!: apply_equality elim!: cons_fun_type)
 
-lemma cons_image_k: "k \<in> n \<Longrightarrow> cons(<n,x>, g)``k = g``k"
+lemma cons_image_k: "k \<in> n \<Longrightarrow> cons(\<langle>n,x\<rangle>, g)``k = g``k"
 by (fast elim: mem_asym)
 
-lemma cons_val_k: "\<lbrakk>k \<in> n; g \<in> n->X\<rbrakk> \<Longrightarrow> cons(<n,x>, g)`k = g`k"
+lemma cons_val_k: "\<lbrakk>k \<in> n; g \<in> n->X\<rbrakk> \<Longrightarrow> cons(\<langle>n,x\<rangle>, g)`k = g`k"
 by (fast intro!: apply_equality consI2 elim!: cons_fun_type apply_Pair)
 
-lemma domain_cons_eq_succ: "domain(f)=x \<Longrightarrow> domain(cons(<x,y>, f)) = succ(x)"
+lemma domain_cons_eq_succ: "domain(f)=x \<Longrightarrow> domain(cons(\<langle>x,y\<rangle>, f)) = succ(x)"
 by (simp add: domain_cons succ_def)
 
-lemma restrict_cons_eq: "g \<in> n->X \<Longrightarrow> restrict(cons(<n,x>, g), n) = g"
+lemma restrict_cons_eq: "g \<in> n->X \<Longrightarrow> restrict(cons(\<langle>n,x\<rangle>, g), n) = g"
 apply (simp add: restrict_def Pi_iff)
 apply (blast intro: elim: mem_irrefl)  
 done
@@ -80,9 +80,9 @@
 
 
 definition
-  DC  :: "i => o"  where
+  DC  :: "i \<Rightarrow> o"  where
     "DC(a) \<equiv> \<forall>X R. R \<subseteq> Pow(X)*X  \<and>
-                    (\<forall>Y \<in> Pow(X). Y \<prec> a \<longrightarrow> (\<exists>x \<in> X. <Y,x> \<in> R)) 
+                    (\<forall>Y \<in> Pow(X). Y \<prec> a \<longrightarrow> (\<exists>x \<in> X. \<langle>Y,x\<rangle> \<in> R)) 
                     \<longrightarrow> (\<exists>f \<in> a->X. \<forall>b<a. <f``b,f`b> \<in> R)"
 
 definition
@@ -91,18 +91,18 @@
                     \<longrightarrow> (\<exists>f \<in> nat->domain(R). \<forall>n \<in> nat. <f`n,f`succ(n)>:R)"
 
 definition
-  ff  :: "[i, i, i, i] => i"  where
+  ff  :: "[i, i, i, i] \<Rightarrow> i"  where
     "ff(b, X, Q, R) \<equiv>
-           transrec(b, %c r. THE x. first(x, {x \<in> X. <r``c, x> \<in> R}, Q))"
+           transrec(b, \<lambda>c r. THE x. first(x, {x \<in> X. <r``c, x> \<in> R}, Q))"
 
 
 locale DC0_imp =
   fixes XX and RR and X and R
 
-  assumes all_ex: "\<forall>Y \<in> Pow(X). Y \<prec> nat \<longrightarrow> (\<exists>x \<in> X. <Y, x> \<in> R)"
+  assumes all_ex: "\<forall>Y \<in> Pow(X). Y \<prec> nat \<longrightarrow> (\<exists>x \<in> X. \<langle>Y, x\<rangle> \<in> R)"
 
   defines XX_def: "XX \<equiv> (\<Union>n \<in> nat. {f \<in> n->X. \<forall>k \<in> n. <f``k, f`k> \<in> R})"
-     and RR_def:  "RR \<equiv> {<z1,z2>:XX*XX. domain(z2)=succ(domain(z1))  
+     and RR_def:  "RR \<equiv> {\<langle>z1,z2\<rangle>:XX*XX. domain(z2)=succ(domain(z1))  
                                        \<and> restrict(z2, domain(z1)) = z1}"
 begin
 
@@ -141,7 +141,7 @@
 apply (erule_tac [2] notE [OF _ empty_subsetI [THEN PowI]])
 apply (erule_tac impE [OF _ nat_0I [THEN n_lesspoll_nat]])
 apply (erule bexE)
-apply (rule_tac a = "<0, {<0, x>}>" in not_emptyI)
+apply (rule_tac a = "<0, {\<langle>0, x\<rangle>}>" in not_emptyI)
 apply (rule CollectI)
 apply (rule SigmaI)
 apply (rule nat_0I [THEN UN_I])
@@ -161,7 +161,7 @@
                                           [OF _ nat_into_Ord] n_lesspoll_nat]],
        assumption+)
 apply (erule bexE)
-apply (rule_tac x = "cons (<n,x>, g) " in exI)
+apply (rule_tac x = "cons (\<langle>n,x\<rangle>, g) " in exI)
 apply (rule CollectI)
 apply (force elim!: cons_fun_type2 
              simp add: cons_image_n cons_val_n cons_image_k cons_val_k)
@@ -266,12 +266,12 @@
                                                                           
     XX = (\<Union>n \<in> nat. {f \<in> succ(n)->domain(R). \<forall>k \<in> n. <f`k, f`succ(k)> \<in> R})
 
-    RR = {<z1,z2>:Fin(XX)*XX. 
+    RR = {\<langle>z1,z2\<rangle>:Fin(XX)*XX. 
            (domain(z2)=succ(\<Union>f \<in> z1. domain(f)) \<and>
             (\<forall>f \<in> z1. restrict(z2, domain(f)) = f)) |      
            (\<not> (\<exists>g \<in> XX. domain(g)=succ(\<Union>f \<in> z1. domain(f)) \<and>
                         (\<forall>f \<in> z1. restrict(g, domain(f)) = f)) \<and>           
-            z2={<0,x>})}                                          
+            z2={\<langle>0,x\<rangle>})}                                          
                                                                           
    Then XX and RR satisfy the hypotheses of DC(omega).                    
    So applying DC:                                                        
@@ -287,7 +287,7 @@
 ************************************************************************* *)
 
 lemma singleton_in_funs: 
- "x \<in> X \<Longrightarrow> {<0,x>} \<in> 
+ "x \<in> X \<Longrightarrow> {\<langle>0,x\<rangle>} \<in> 
             (\<Union>n \<in> nat. {f \<in> succ(n)->X. \<forall>k \<in> n. <f`k, f`succ(k)> \<in> R})"
 apply (rule nat_0I [THEN UN_I])
 apply (force simp add: singleton_0 [symmetric]
@@ -300,15 +300,15 @@
   defines XX_def: "XX \<equiv> (\<Union>n \<in> nat.
                       {f \<in> succ(n)->domain(R). \<forall>k \<in> n. <f`k, f`succ(k)> \<in> R})"
       and RR_def:
-         "RR \<equiv> {<z1,z2>:Fin(XX)*XX. 
+         "RR \<equiv> {\<langle>z1,z2\<rangle>:Fin(XX)*XX. 
                   (domain(z2)=succ(\<Union>f \<in> z1. domain(f))  
                     \<and> (\<forall>f \<in> z1. restrict(z2, domain(f)) = f))
                   | (\<not> (\<exists>g \<in> XX. domain(g)=succ(\<Union>f \<in> z1. domain(f))  
-                     \<and> (\<forall>f \<in> z1. restrict(g, domain(f)) = f)) \<and> z2={<0,x>})}"
+                     \<and> (\<forall>f \<in> z1. restrict(g, domain(f)) = f)) \<and> z2={\<langle>0,x\<rangle>})}"
       and allRR_def:
         "allRR \<equiv> \<forall>b<nat.
                    <f``b, f`b> \<in>  
-                    {<z1,z2>\<in>Fin(XX)*XX. (domain(z2)=succ(\<Union>f \<in> z1. domain(f))
+                    {\<langle>z1,z2\<rangle>\<in>Fin(XX)*XX. (domain(z2)=succ(\<Union>f \<in> z1. domain(f))
                                     \<and> (\<Union>f \<in> z1. domain(f)) = b  
                                     \<and> (\<forall>f \<in> z1. restrict(z2,domain(f)) = f))}"
 begin
@@ -316,7 +316,7 @@
 lemma lemma4:
      "\<lbrakk>range(R) \<subseteq> domain(R);  x \<in> domain(R)\<rbrakk>   
       \<Longrightarrow> RR \<subseteq> Pow(XX)*XX \<and>   
-             (\<forall>Y \<in> Pow(XX). Y \<prec> nat \<longrightarrow> (\<exists>x \<in> XX. <Y,x>:RR))"
+             (\<forall>Y \<in> Pow(XX). Y \<prec> nat \<longrightarrow> (\<exists>x \<in> XX. \<langle>Y,x\<rangle>:RR))"
 apply (rule conjI)
 apply (force dest!: FinD [THEN PowI] simp add: RR_def)
 apply (rule impI [THEN ballI])
@@ -368,7 +368,7 @@
 
 lemma restrict_cons_eq_restrict: 
      "\<lbrakk>restrict(h, domain(u))=u;  h \<in> n->X;  domain(u) \<subseteq> n\<rbrakk>   
-      \<Longrightarrow> restrict(cons(<n, y>, h), domain(u)) = u"
+      \<Longrightarrow> restrict(cons(\<langle>n, y\<rangle>, h), domain(u)) = u"
 apply (unfold restrict_def)
 apply (simp add: restrict_def Pi_iff)
 apply (erule sym [THEN trans, symmetric])
@@ -512,7 +512,7 @@
 apply (erule allE impE)+
 apply (rule Card_Hartog)
 apply (erule_tac x = A in allE)
-apply (erule_tac x = "{<z1,z2> \<in> Pow (A) *A . z1 \<prec> Hartog (A) \<and> z2 \<notin> z1}" 
+apply (erule_tac x = "{\<langle>z1,z2\<rangle> \<in> Pow (A) *A . z1 \<prec> Hartog (A) \<and> z2 \<notin> z1}" 
                  in allE)
 apply simp
 apply (erule impE, fast elim: lesspoll_lemma [THEN not_emptyE])
@@ -549,15 +549,15 @@
 by (fast intro!: lam_type RepFunI)
 
 lemma lemmaX:
-     "\<lbrakk>\<forall>Y \<in> Pow(X). Y \<prec> K \<longrightarrow> (\<exists>x \<in> X. <Y, x> \<in> R);   
+     "\<lbrakk>\<forall>Y \<in> Pow(X). Y \<prec> K \<longrightarrow> (\<exists>x \<in> X. \<langle>Y, x\<rangle> \<in> R);   
          b \<in> K; Z \<in> Pow(X); Z \<prec> K\<rbrakk>   
-      \<Longrightarrow> {x \<in> X. <Z,x> \<in> R} \<noteq> 0"
+      \<Longrightarrow> {x \<in> X. \<langle>Z,x\<rangle> \<in> R} \<noteq> 0"
 by blast
 
 
 lemma WO1_DC_lemma:
      "\<lbrakk>Card(K); well_ord(X,Q);   
-         \<forall>Y \<in> Pow(X). Y \<prec> K \<longrightarrow> (\<exists>x \<in> X. <Y, x> \<in> R); b \<in> K\<rbrakk>   
+         \<forall>Y \<in> Pow(X). Y \<prec> K \<longrightarrow> (\<exists>x \<in> X. \<langle>Y, x\<rangle> \<in> R); b \<in> K\<rbrakk>   
       \<Longrightarrow> ff(b, X, Q, R) \<in> {x \<in> X. <(\<lambda>c \<in> b. ff(c, X, Q, R))``b, x> \<in> R}"
 apply (rule_tac P = "b \<in> K" in impE, (erule_tac [2] asm_rl)+)
 apply (rule_tac i=b in Card_is_Ord [THEN Ord_in_Ord, THEN trans_induct],