diff -r e8da2cfdfcff src/ZF/Cardinal.thy
--- a/src/ZF/Cardinal.thy	Sat Nov 28 13:49:46 2020 +0100
+++ b/src/ZF/Cardinal.thy	Sat Nov 28 17:58:49 2020 -0300
@@ -329,7 +329,7 @@
 lemma Least_cong: "(!!y. P(y) \<longleftrightarrow> Q(y)) ==> (\<mu> x. P(x)) = (\<mu> x. Q(x))"
 by simp
 
-(*Need AC to get @{term"X \<lesssim> Y ==> |X| \<le> |Y|"};  see well_ord_lepoll_imp_Card_le
+(*Need AC to get @{term"X \<lesssim> Y ==> |X| \<le> |Y|"};  see well_ord_lepoll_imp_cardinal_le
   Converse also requires AC, but see well_ord_cardinal_eqE*)
 lemma cardinal_cong: "X \<approx> Y ==> |X| = |Y|"
 apply (unfold eqpoll_def cardinal_def)
@@ -507,7 +507,7 @@
 by (simp add: Card_lt_iff Card_is_Ord Ord_cardinal not_lt_iff_le [THEN iff_sym])
 
 (*Can use AC or finiteness to discharge first premise*)
-lemma well_ord_lepoll_imp_Card_le:
+lemma well_ord_lepoll_imp_cardinal_le:
   assumes wB: "well_ord(B,r)" and AB: "A \<lesssim> B"
   shows "|A| \<le> |B|"
 using Ord_cardinal [of A] Ord_cardinal [of B]
@@ -528,7 +528,7 @@
 
 lemma lepoll_cardinal_le: "[| A \<lesssim> i; Ord(i) |] ==> |A| \<le> i"
 apply (rule le_trans)
-apply (erule well_ord_Memrel [THEN well_ord_lepoll_imp_Card_le], assumption)
+apply (erule well_ord_Memrel [THEN well_ord_lepoll_imp_cardinal_le], assumption)
 apply (erule Ord_cardinal_le)
 done
 
diff -r e8da2cfdfcff src/ZF/CardinalArith.thy
--- a/src/ZF/CardinalArith.thy	Sat Nov 28 13:49:46 2020 +0100
+++ b/src/ZF/CardinalArith.thy	Sat Nov 28 17:58:49 2020 -0300
@@ -151,7 +151,7 @@
   have "K \<le> |K|"
     by (rule Card_cardinal_le [OF K])
   moreover have "|K| \<le> |K + L|" using K L
-    by (blast intro: well_ord_lepoll_imp_Card_le sum_lepoll_self
+    by (blast intro: well_ord_lepoll_imp_cardinal_le sum_lepoll_self
                      well_ord_radd well_ord_Memrel Card_is_Ord)
   ultimately show "K \<le> |K + L|"
     by (blast intro: le_trans)
@@ -173,7 +173,7 @@
     "[| K' \<le> K;  L' \<le> L |] ==> (K' \<oplus> L') \<le> (K \<oplus> L)"
 apply (unfold cadd_def)
 apply (safe dest!: le_subset_iff [THEN iffD1])
-apply (rule well_ord_lepoll_imp_Card_le)
+apply (rule well_ord_lepoll_imp_cardinal_le)
 apply (blast intro: well_ord_radd well_ord_Memrel)
 apply (blast intro: sum_lepoll_mono subset_imp_lepoll)
 done
@@ -308,7 +308,7 @@
 lemma cmult_square_le: "Card(K) ==> K \<le> K \<otimes> K"
 apply (unfold cmult_def)
 apply (rule le_trans)
-apply (rule_tac [2] well_ord_lepoll_imp_Card_le)
+apply (rule_tac [2] well_ord_lepoll_imp_cardinal_le)
 apply (rule_tac [3] prod_square_lepoll)
 apply (simp add: le_refl Card_is_Ord Card_cardinal_eq)
 apply (blast intro: well_ord_rmult well_ord_Memrel Card_is_Ord)
@@ -325,7 +325,7 @@
 lemma cmult_le_self:
     "[| Card(K);  Ord(L);  0<L |] ==> K \<le> (K \<otimes> L)"
 apply (unfold cmult_def)
-apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_Card_le])
+apply (rule le_trans [OF Card_cardinal_le well_ord_lepoll_imp_cardinal_le])
   apply assumption
  apply (blast intro: well_ord_rmult well_ord_Memrel Card_is_Ord)
 apply (blast intro: prod_lepoll_self ltD)
@@ -347,7 +347,7 @@
     "[| K' \<le> K;  L' \<le> L |] ==> (K' \<otimes> L') \<le> (K \<otimes> L)"
 apply (unfold cmult_def)
 apply (safe dest!: le_subset_iff [THEN iffD1])
-apply (rule well_ord_lepoll_imp_Card_le)
+apply (rule well_ord_lepoll_imp_cardinal_le)
  apply (blast intro: well_ord_rmult well_ord_Memrel)
 apply (blast intro: prod_lepoll_mono subset_imp_lepoll)
 done
@@ -548,7 +548,7 @@
   assumes K: "Limit(K)" and x: "x<K" and y: " y<K"
   defines "z \<equiv> succ(x \<union> y)"
   shows "|ordermap(K \<times> K, csquare_rel(K)) ` \<langle>x,y\<rangle>| \<le> |succ(z)| \<otimes> |succ(z)|"
-proof (unfold cmult_def, rule well_ord_lepoll_imp_Card_le)
+proof (unfold cmult_def, rule well_ord_lepoll_imp_cardinal_le)
   show "well_ord(|succ(z)| \<times> |succ(z)|,
                  rmult(|succ(z)|, Memrel(|succ(z)|), |succ(z)|, Memrel(|succ(z)|)))"
     by (blast intro: Ord_cardinal well_ord_Memrel well_ord_rmult)
@@ -627,9 +627,10 @@
 
 (*Main result: Kunen's Theorem 10.12*)
 lemma InfCard_csquare_eq:
-  assumes IK: "InfCard(K)" shows "InfCard(K) ==> K \<otimes> K = K"
+ shows "InfCard(K) ==> K \<otimes> K = K"
 proof -
-  have  OK: "Ord(K)" using IK by (simp add: Card_is_Ord InfCard_is_Card)
+  assume "InfCard(K)"
+  then have OK: "Ord(K)" by (simp add: Card_is_Ord InfCard_is_Card)
   show "InfCard(K) ==> K \<otimes> K = K" using OK
   proof (induct rule: trans_induct)
     case (step i)
diff -r e8da2cfdfcff src/ZF/Cardinal_AC.thy
--- a/src/ZF/Cardinal_AC.thy	Sat Nov 28 13:49:46 2020 +0100
+++ b/src/ZF/Cardinal_AC.thy	Sat Nov 28 17:58:49 2020 -0300
@@ -33,9 +33,9 @@
       ==> |A \<union> C| = |B \<union> D|"
 by (simp add: cardinal_eqpoll_iff eqpoll_disjoint_Un)
 
-lemma lepoll_imp_Card_le: "A \<lesssim> B ==> |A| \<le> |B|"
+lemma lepoll_imp_cardinal_le: "A \<lesssim> B ==> |A| \<le> |B|"
 apply (rule AC_well_ord [THEN exE])
-apply (erule well_ord_lepoll_imp_Card_le, assumption)
+apply (erule well_ord_lepoll_imp_cardinal_le, assumption)
 done
 
 lemma cadd_assoc: "(i \<oplus> j) \<oplus> k = i \<oplus> (j \<oplus> k)"
@@ -82,7 +82,7 @@
 lemma le_Card_iff: "Card(K) ==> |A| \<le> K \<longleftrightarrow> A \<lesssim> K"
 apply (erule Card_cardinal_eq [THEN subst], rule iffI,
        erule Card_le_imp_lepoll)
-apply (erule lepoll_imp_Card_le)
+apply (erule lepoll_imp_cardinal_le)
 done
 
 lemma cardinal_0_iff_0 [simp]: "|A| = 0 \<longleftrightarrow> A = 0"
@@ -132,7 +132,7 @@
 text\<open>Kunen's Lemma 10.20\<close>
 lemma surj_implies_cardinal_le: 
   assumes f: "f \<in> surj(X,Y)" shows "|Y| \<le> |X|"
-proof (rule lepoll_imp_Card_le)
+proof (rule lepoll_imp_cardinal_le)
   from f [THEN surj_implies_inj] obtain g where "g \<in> inj(Y,X)" ..
   thus "Y \<lesssim> X"
     by (auto simp add: lepoll_def)
diff -r e8da2cfdfcff src/ZF/Constructible/Formula.thy
--- a/src/ZF/Constructible/Formula.thy	Sat Nov 28 13:49:46 2020 +0100
+++ b/src/ZF/Constructible/Formula.thy	Sat Nov 28 17:58:49 2020 -0300
@@ -87,12 +87,12 @@
   sats :: "[i,i,i] => o" where
   "sats(A,p,env) == satisfies(A,p)`env = 1"
 
-lemma [simp]:
+lemma sats_Member_iff [simp]:
   "env \<in> list(A)
    ==> sats(A, Member(x,y), env) \<longleftrightarrow> nth(x,env) \<in> nth(y,env)"
 by simp
 
-lemma [simp]:
+lemma sats_Equal_iff [simp]:
   "env \<in> list(A)
    ==> sats(A, Equal(x,y), env) \<longleftrightarrow> nth(x,env) = nth(y,env)"
 by simp
diff -r e8da2cfdfcff src/ZF/Constructible/L_axioms.thy
--- a/src/ZF/Constructible/L_axioms.thy	Sat Nov 28 13:49:46 2020 +0100
+++ b/src/ZF/Constructible/L_axioms.thy	Sat Nov 28 17:58:49 2020 -0300
@@ -739,7 +739,7 @@
                   Exists(And(Member(0,succ(succ(r))),
                              Exists(pair_fm(0,2,1))))))"
 
-lemma range_type [TC]:
+lemma range_fm_type [TC]:
      "[| x \<in> nat; y \<in> nat |] ==> range_fm(x,y) \<in> formula"
 by (simp add: range_fm_def)
 
diff -r e8da2cfdfcff src/ZF/Constructible/Rank.thy
--- a/src/ZF/Constructible/Rank.thy	Sat Nov 28 13:49:46 2020 +0100
+++ b/src/ZF/Constructible/Rank.thy	Sat Nov 28 17:58:49 2020 -0300
@@ -137,7 +137,7 @@
 
 definition  
   obase :: "[i=>o,i,i] => i" where
-       \<comment> \<open>the domain of \<open>om\<close>, eventually shown to equal \<open>A\<close>\<close>
+       \<comment> \<open>the domain of \<open>omap\<close>, eventually shown to equal \<open>A\<close>\<close>
    "obase(M,A,r) == {a\<in>A. \<exists>x[M]. \<exists>g[M]. Ord(x) & 
                           g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x))}"
 
@@ -156,7 +156,7 @@
 
 text\<open>Can also be proved with the premise \<^term>\<open>M(z)\<close> instead of
       \<^term>\<open>M(f)\<close>, but that version is less useful.  This lemma
-      is also more useful than the definition, \<open>omap_def\<close>.\<close>
+      is also more useful than the definition, @{thm omap_def}.\<close>
 lemma (in M_ordertype) omap_iff:
      "[| omap(M,A,r,f); M(A); M(f) |] 
       ==> z \<in> f \<longleftrightarrow>
@@ -256,7 +256,7 @@
 done
 
 
-text\<open>This is not the final result: we must show \<^term>\<open>oB(A,r) = A\<close>\<close>
+text\<open>This is not the final result: we must show \<^term>\<open>obase(M,A,r) = A\<close>\<close>
 lemma (in M_ordertype) omap_ord_iso:
      "[| wellordered(M,A,r); omap(M,A,r,f); otype(M,A,r,i); 
        M(A); M(r); M(f); M(i) |] ==> f \<in> ord_iso(obase(M,A,r),r,i,Memrel(i))"
@@ -331,7 +331,7 @@
 
 
 
-text\<open>Main result: \<^term>\<open>om\<close> gives the order-isomorphism 
+text\<open>Main result: \<^term>\<open>omap\<close> gives the order-isomorphism 
       \<^term>\<open>\<langle>A,r\<rangle> \<cong> \<langle>i, Memrel(i)\<rangle>\<close>\<close>
 theorem (in M_ordertype) omap_ord_iso_otype:
      "[| wellordered(M,A,r); omap(M,A,r,f); otype(M,A,r,i);
@@ -340,7 +340,7 @@
 apply (simp add: obase_equals)  
 done 
 
-lemma (in M_ordertype) obase_exists:
+lemma (in M_ordertype) obase_closed:
      "[| M(A); M(r) |] ==> M(obase(M,A,r))"
 apply (simp add: obase_def) 
 apply (insert obase_separation [of A r])
@@ -353,7 +353,7 @@
 apply (insert omap_replacement [of A r])
 apply (simp add: strong_replacement_def) 
 apply (drule_tac x="obase(M,A,r)" in rspec) 
- apply (simp add: obase_exists) 
+ apply (simp add: obase_closed) 
 apply (simp add: obase_def)
 apply (erule impE) 
  apply (clarsimp simp add: univalent_def)
@@ -373,7 +373,7 @@
 lemma (in M_ordertype) ordertype_exists:
      "[| wellordered(M,A,r); M(A); M(r) |]
       ==> \<exists>f[M]. (\<exists>i[M]. Ord(i) & f \<in> ord_iso(A, r, i, Memrel(i)))"
-apply (insert obase_exists [of A r] omap_exists [of A r] otype_exists [of A r], simp, clarify)
+apply (insert obase_closed [of A r] omap_exists [of A r] otype_exists [of A r], simp, clarify)
 apply (rename_tac i) 
 apply (subgoal_tac "Ord(i)", blast intro: omap_ord_iso_otype)
 apply (rule Ord_otype) 
@@ -397,7 +397,7 @@
 
 
 text\<open>(b) Order types are absolute\<close>
-theorem (in M_ordertype) 
+theorem (in M_ordertype) ordertypes_are_absolute:
      "[| wellordered(M,A,r); f \<in> ord_iso(A, r, i, Memrel(i));
        M(A); M(r); M(f); M(i); Ord(i) |] ==> i = ordertype(A,r)"
 by (blast intro: Ord_ordertype relativized_imp_well_ord ordertype_ord_iso
diff -r e8da2cfdfcff src/ZF/Constructible/Relative.thy
--- a/src/ZF/Constructible/Relative.thy	Sat Nov 28 13:49:46 2020 +0100
+++ b/src/ZF/Constructible/Relative.thy	Sat Nov 28 17:58:49 2020 -0300
@@ -715,7 +715,7 @@
 
 subsubsection\<open>Absoluteness for Separation and Replacement\<close>
 
-lemma (in M_trans) separation_closed [intro,simp]:
+lemma (in M_trans) Collect_closed [intro,simp]:
      "[| separation(M,P); M(A) |] ==> M(Collect(A,P))"
 apply (insert separation, simp add: separation_def)
 apply (drule rspec, assumption, clarify)
@@ -1343,7 +1343,7 @@
 
 lemma (in M_basic) separation_conj:
      "[|separation(M,P); separation(M,Q)|] ==> separation(M, \<lambda>z. P(z) & Q(z))"
-by (simp del: separation_closed
+by (simp del: Collect_closed
          add: separation_iff Collect_Int_Collect_eq [symmetric])
 
 (*???equalities*)
@@ -1363,12 +1363,12 @@
 
 lemma (in M_basic) separation_disj:
      "[|separation(M,P); separation(M,Q)|] ==> separation(M, \<lambda>z. P(z) | Q(z))"
-by (simp del: separation_closed
+by (simp del: Collect_closed
          add: separation_iff Collect_Un_Collect_eq [symmetric])
 
 lemma (in M_basic) separation_neg:
      "separation(M,P) ==> separation(M, \<lambda>z. ~P(z))"
-by (simp del: separation_closed
+by (simp del: Collect_closed
          add: separation_iff Diff_Collect_eq [symmetric])
 
 lemma (in M_basic) separation_imp:
@@ -1383,7 +1383,7 @@
      "[|M(Y); \<forall>y[M]. separation(M, \<lambda>x. P(x,y));
         \<forall>z[M]. strong_replacement(M, \<lambda>x y. y = {u \<in> z . P(u,x)})|]
       ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>Y \<longrightarrow> P(x,y))"
-apply (simp del: separation_closed rall_abs
+apply (simp del: Collect_closed rall_abs
          add: separation_iff Collect_rall_eq)
 apply (blast intro!:  RepFun_closed dest: transM)
 done
diff -r e8da2cfdfcff src/ZF/Constructible/Wellorderings.thy
--- a/src/ZF/Constructible/Wellorderings.thy	Sat Nov 28 13:49:46 2020 +0100
+++ b/src/ZF/Constructible/Wellorderings.thy	Sat Nov 28 17:58:49 2020 -0300
@@ -164,7 +164,7 @@
       ==> order_isomorphism(M,A,r,B,s,f) \<longleftrightarrow> f \<in> ord_iso(A,r,B,s)"
 by (simp add: order_isomorphism_def ord_iso_def)
 
-lemma (in M_basic) pred_set_abs [simp]: 
+lemma (in M_trans) pred_set_abs [simp]: 
      "[| M(r); M(B) |] ==> pred_set(M,A,x,r,B) \<longleftrightarrow> B = Order.pred(A,x,r)"
 apply (simp add: pred_set_def Order.pred_def)
 apply (blast dest: transM) 
diff -r e8da2cfdfcff src/ZF/InfDatatype.thy
--- a/src/ZF/InfDatatype.thy	Sat Nov 28 13:49:46 2020 +0100
+++ b/src/ZF/InfDatatype.thy	Sat Nov 28 17:58:49 2020 -0300
@@ -103,7 +103,7 @@
 lemmas le_nat_Un_cardinal =
      Un_upper2_le [OF Ord_nat Card_cardinal [THEN Card_is_Ord]]
 
-lemmas UN_upper_cardinal = UN_upper [THEN subset_imp_lepoll, THEN lepoll_imp_Card_le]
+lemmas UN_upper_cardinal = UN_upper [THEN subset_imp_lepoll, THEN lepoll_imp_cardinal_le]
 
 (*The new version of Data_Arg.intrs, declared in Datatype.ML*)
 lemmas Data_Arg_intros =
diff -r e8da2cfdfcff src/ZF/ZF_Base.thy
--- a/src/ZF/ZF_Base.thy	Sat Nov 28 13:49:46 2020 +0100
+++ b/src/ZF/ZF_Base.thy	Sat Nov 28 17:58:49 2020 -0300
@@ -85,8 +85,8 @@
   where "\<Inter>(A) == { x\<in>\<Union>(A) . \<forall>y\<in>A. x\<in>y}"
 
 syntax
-  "_UNION" :: "[pttrn, i, i] => i"  (\<open>(3\<Union>_\<in>_./ _)\<close> 10)
-  "_INTER" :: "[pttrn, i, i] => i"  (\<open>(3\<Inter>_\<in>_./ _)\<close> 10)
+  "_UNION" :: "[pttrn, i, i] => i"  (\<open>(3\<Union>_\<in>_./ _)\<close> 51)
+  "_INTER" :: "[pttrn, i, i] => i"  (\<open>(3\<Inter>_\<in>_./ _)\<close> 51)
 translations
   "\<Union>x\<in>A. B" == "CONST Union({B. x\<in>A})"
   "\<Inter>x\<in>A. B" == "CONST Inter({B. x\<in>A})"
@@ -249,9 +249,9 @@
 (* binder syntax *)
 
 syntax
-  "_PROD"     :: "[pttrn, i, i] => i"        (\<open>(3\<Prod>_\<in>_./ _)\<close> 10)
-  "_SUM"      :: "[pttrn, i, i] => i"        (\<open>(3\<Sum>_\<in>_./ _)\<close> 10)
-  "_lam"      :: "[pttrn, i, i] => i"        (\<open>(3\<lambda>_\<in>_./ _)\<close> 10)
+  "_PROD"     :: "[pttrn, i, i] => i"        (\<open>(3\<Prod>_\<in>_./ _)\<close> 51)
+  "_SUM"      :: "[pttrn, i, i] => i"        (\<open>(3\<Sum>_\<in>_./ _)\<close> 51)
+  "_lam"      :: "[pttrn, i, i] => i"        (\<open>(3\<lambda>_\<in>_./ _)\<close> 51)
 translations
   "\<Prod>x\<in>A. B"   == "CONST Pi(A, \<lambda>x. B)"
   "\<Sum>x\<in>A. B"   == "CONST Sigma(A, \<lambda>x. B)"