# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1664297660 -3600
# Node ID 9fc34f76b4e85939fe6c910790aaadde2f3a828c
# Parent  a642599ffdea7b0df43f7b210c08e6f62b58378e
getting rid of apply (unfold ...)

diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/AC/AC15_WO6.thy
--- a/src/ZF/AC/AC15_WO6.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/AC15_WO6.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -32,7 +32,7 @@
 (* ********************************************************************** *)
 
 lemma lepoll_Sigma: "A\<noteq>0 \<Longrightarrow> B \<lesssim> A*B"
-apply (unfold lepoll_def)
+  unfolding lepoll_def
 apply (erule not_emptyE)
 apply (rule_tac x = "\<lambda>z \<in> B. \<langle>x,z\<rangle>" in exI)
 apply (fast intro!: snd_conv lam_injective)
@@ -58,14 +58,14 @@
              sets_of_size_between(f`B, 2, n) \<and> \<Union>(f`B)=B   
      \<Longrightarrow> \<forall>B \<in> A. \<exists>! u. u \<in> f`cons(0, B*nat) \<and> u \<subseteq> cons(0, B*nat) \<and>   
              0 \<in> u \<and> 2 \<lesssim> u \<and> u \<lesssim> n"
-apply (unfold sets_of_size_between_def)
+  unfolding sets_of_size_between_def
 apply (rule ballI)
 apply (erule_tac x="cons(0, B*nat)" in ballE)
  apply (blast dest: lemma1 intro!: lemma2, blast)
 done
 
 lemma lemma4: "\<lbrakk>A \<lesssim> i; Ord(i)\<rbrakk> \<Longrightarrow> {P(a). a \<in> A} \<lesssim> i"
-apply (unfold lepoll_def)
+  unfolding lepoll_def
 apply (erule exE)
 apply (rule_tac x = "\<lambda>x \<in> RepFun(A,P). \<mu> j. \<exists>a\<in>A. x=P(a) \<and> f`a=j" 
        in exI)
@@ -227,7 +227,7 @@
 (* ********************************************************************** *)
 
 lemma AC13_mono: "\<lbrakk>m\<le>n; AC13(m)\<rbrakk> \<Longrightarrow> AC13(n)"
-apply (unfold AC13_def)
+  unfolding AC13_def
 apply (drule le_imp_lepoll)
 apply (fast elim!: lepoll_trans)
 done
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/AC/AC16_WO4.thy
--- a/src/ZF/AC/AC16_WO4.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/AC16_WO4.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -18,7 +18,7 @@
      "\<lbrakk>Finite(A); 0<m; m \<in> nat\<rbrakk> 
       \<Longrightarrow> \<exists>a f. Ord(a) \<and> domain(f) = a \<and>   
                 (\<Union>b<a. f`b) = A \<and> (\<forall>b<a. f`b \<lesssim> m)"
-apply (unfold Finite_def)
+  unfolding Finite_def
 apply (erule bexE)
 apply (drule eqpoll_sym [THEN eqpoll_def [THEN def_imp_iff, THEN iffD1]])
 apply (erule exE)
@@ -345,7 +345,7 @@
      "\<lbrakk>z \<in> xa \<inter> (x - {u}); l \<approx> a; a \<subseteq> y; u \<in> x\<rbrakk>   
       \<Longrightarrow> \<exists>! w. w \<in> t_n \<and> cons(z, cons(u, a)) \<subseteq> w"
 apply (rule all_ex [THEN bspec])
-apply (unfold k_def)
+  unfolding k_def
 apply (fast intro!: cons_eqpoll_succ elim: eqpoll_sym)
 done
 
@@ -442,12 +442,12 @@
 lemma the_in_MM_subset:
      "v \<in> LL \<Longrightarrow> (THE x. x \<in> MM \<and> v \<subseteq> x) \<subseteq> x \<union> y"
 apply (drule unique_superset1)
-apply (unfold MM_def)
+  unfolding MM_def
 apply (fast dest!: unique_superset1 "includes" [THEN subsetD])
 done
 
 lemma GG_subset: "v \<in> LL \<Longrightarrow> GG ` v \<subseteq> x"
-apply (unfold GG_def)
+  unfolding GG_def
 apply (frule the_in_MM_subset)
 apply (frule in_LL_eq_Int)
 apply (force elim: equalityE)
@@ -473,7 +473,7 @@
 apply (rule ccontr)
 apply (subgoal_tac "\<forall>v \<in> s (u) . k \<approx> v \<inter> y")
 prefer 2 apply (simp add: s_def, blast intro: succ_not_lepoll_imp_eqpoll)
-apply (unfold k_def)
+  unfolding k_def
 apply (insert all_ex "includes" lnat)
 apply (rule ex_subset_eqpoll_n [THEN exE], assumption)
 apply (rule noLepoll [THEN notE])
@@ -489,7 +489,7 @@
 apply (rule exists_in_MM [THEN bexE], assumption)
 apply (rule bexI)
 apply (erule_tac [2] Int_in_LL)
-apply (unfold GG_def)
+  unfolding GG_def
 apply (simp add: Int_in_LL)
 apply (subst unique_superset_in_MM [THEN the_equality2])
 apply (fast elim!: Int_in_LL)+
@@ -516,7 +516,7 @@
 (* ********************************************************************** *)
 
 lemma in_MM_eqpoll_n: "w \<in> MM \<Longrightarrow> w \<approx> succ(k #+ m)"
-apply (unfold MM_def)
+  unfolding MM_def
 apply (fast dest: "includes" [THEN subsetD])
 done
 
@@ -529,7 +529,7 @@
 lemma all_in_lepoll_m: 
       "well_ord(LL,S) \<Longrightarrow>       
        \<forall>b<ordertype(LL,S). GG ` (converse(ordermap(LL,S)) ` b) \<lesssim> m"
-apply (unfold GG_def)
+  unfolding GG_def
 apply (rule oallI)
 apply (simp add: ltD ordermap_bij [THEN bij_converse_bij, THEN bij_is_fun, THEN apply_type])
 apply (insert "includes")
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/AC/AC16_lemmas.thy
--- a/src/ZF/AC/AC16_lemmas.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/AC16_lemmas.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -12,7 +12,7 @@
 by fast
 
 lemma nat_1_lepoll_iff: "1\<lesssim>X \<longleftrightarrow> (\<exists>x. x \<in> X)"
-apply (unfold lepoll_def)
+  unfolding lepoll_def
 apply (rule iffI)
 apply (fast intro: inj_is_fun [THEN apply_type])
 apply (erule exE)
@@ -29,7 +29,7 @@
 done
 
 lemma cons_eqpoll_succ: "\<lbrakk>x\<approx>n; y\<notin>x\<rbrakk> \<Longrightarrow> cons(y,x)\<approx>succ(n)"
-apply (unfold succ_def)
+  unfolding succ_def
 apply (fast elim!: cons_eqpoll_cong mem_irrefl)
 done
 
@@ -71,7 +71,7 @@
 lemma subsets_lepoll_lemma1:
      "\<lbrakk>InfCard(x); n \<in> nat\<rbrakk> 
       \<Longrightarrow> {y \<in> Pow(x). y\<approx>succ(succ(n))} \<lesssim> x*{y \<in> Pow(x). y\<approx>succ(n)}"
-apply (unfold lepoll_def)
+  unfolding lepoll_def
 apply (rule_tac x = "\<lambda>y \<in> {y \<in> Pow(x) . y\<approx>succ (succ (n))}. 
                       <\<mu> i. i \<in> y, y-{\<mu> i. i \<in> y}>" in exI)
 apply (rule_tac d = "\<lambda>z. cons (fst(z), snd(z))" in lam_injective)
@@ -144,7 +144,7 @@
 lemma succ_lepoll_succ_succ:
      "\<lbrakk>InfCard(x); n \<in> nat\<rbrakk> 
       \<Longrightarrow> {y \<in> Pow(x). y\<approx>succ(n)} \<lesssim> {y \<in> Pow(x). y\<approx>succ(succ(n))}"
-apply (unfold lepoll_def)
+  unfolding lepoll_def
 apply (rule_tac x = "\<lambda>z \<in> {y\<in>Pow(x). y\<approx>succ(n)}. cons(succ(\<Union>(z)), z)" 
        in exI)
 apply (rule_tac d = "\<lambda>z. z-{\<Union>(z) }" in lam_injective)
@@ -173,7 +173,7 @@
 
 lemma image_vimage_eq:
      "\<lbrakk>f \<in> surj(A,B); y \<subseteq> B\<rbrakk> \<Longrightarrow> f``(converse(f)``y) = y"
-apply (unfold surj_def)
+  unfolding surj_def
 apply (fast dest: apply_equality2 elim: apply_iff [THEN iffD2])
 done
 
@@ -182,7 +182,7 @@
 
 lemma subsets_eqpoll:
      "A\<approx>B \<Longrightarrow> {Y \<in> Pow(A). Y\<approx>n}\<approx>{Y \<in> Pow(B). Y\<approx>n}"
-apply (unfold eqpoll_def)
+  unfolding eqpoll_def
 apply (erule exE)
 apply (rule_tac x = "\<lambda>X \<in> {Y \<in> Pow (A) . \<exists>f. f \<in> bij (Y, n) }. f``X" in exI)
 apply (rule_tac d = "\<lambda>Z. converse (f) ``Z" in lam_bijective)
@@ -197,7 +197,7 @@
 done
 
 lemma WO2_imp_ex_Card: "WO2 \<Longrightarrow> \<exists>a. Card(a) \<and> X\<approx>a"
-apply (unfold WO2_def)
+  unfolding WO2_def
 apply (drule spec [of _ X])
 apply (blast intro: Card_cardinal eqpoll_trans
           well_ord_Memrel [THEN well_ord_cardinal_eqpoll, THEN eqpoll_sym])
@@ -207,7 +207,7 @@
 by (blast intro: lepoll_Finite)
 
 lemma infinite_Card_is_InfCard: "\<lbrakk>\<not>Finite(X); Card(X)\<rbrakk> \<Longrightarrow> InfCard(X)"
-apply (unfold InfCard_def)
+  unfolding InfCard_def
 apply (fast elim!: Card_is_Ord [THEN nat_le_infinite_Ord])
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/AC/AC17_AC1.thy
--- a/src/ZF/AC/AC17_AC1.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/AC17_AC1.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -71,7 +71,7 @@
 
 lemma not_AC1_imp_ex:
      "\<not>AC1 \<Longrightarrow> \<exists>A. \<forall>f \<in> Pow(A)-{0} -> A. \<exists>u \<in> Pow(A)-{0}. f`u \<notin> u"
-apply (unfold AC1_def)
+  unfolding AC1_def
 apply (erule swap)
 apply (rule allI)
 apply (erule swap)
@@ -112,7 +112,7 @@
 by simp
 
 lemma AC17_AC1: "AC17 \<Longrightarrow> AC1"
-apply (unfold AC17_def)
+  unfolding AC17_def
 apply (rule classical)
 apply (erule not_AC1_imp_ex [THEN exE])
 apply (case_tac 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/AC/AC18_AC19.thy
--- a/src/ZF/AC/AC18_AC19.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/AC18_AC19.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -36,7 +36,7 @@
 done
 
 lemma AC1_AC18: "AC1 \<Longrightarrow> PROP AC18"
-apply (unfold AC1_def)
+  unfolding AC1_def
 apply (rule AC18.intro)
 apply (fast elim!: lemma_AC18 apply_type intro!: equalityI INT_I UN_I)
 done
@@ -46,7 +46,7 @@
 (* ********************************************************************** *)
 
 theorem (in AC18) AC19
-apply (unfold AC19_def)
+  unfolding AC19_def
 apply (intro allI impI)
 apply (rule AC18 [of _ "\<lambda>x. x", THEN mp], blast)
 done
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/AC/AC7_AC9.thy
--- a/src/ZF/AC/AC7_AC9.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/AC7_AC9.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -22,7 +22,7 @@
         "C \<in> A \<Longrightarrow> (\<lambda>g \<in> (nat->\<Union>(A))*C.   
                 (\<lambda>n \<in> nat. if(n=0, snd(g), fst(g)`(n #- 1))))   
                 \<in> inj((nat->\<Union>(A))*C, (nat->\<Union>(A)) ) "
-apply (unfold inj_def)
+  unfolding inj_def
 apply (rule CollectI)
 apply (fast intro!: lam_type if_type apply_type fst_type snd_type, auto) 
 apply (rule fun_extension, assumption+)
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/AC/AC_Equiv.thy
--- a/src/ZF/AC/AC_Equiv.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/AC_Equiv.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -138,7 +138,7 @@
 
 (* lemma for ordertype_Int *)
 lemma rvimage_id: "rvimage(A,id(A),r) = r \<inter> A*A"
-apply (unfold rvimage_def)
+  unfolding rvimage_def
 apply (rule equalityI, safe)
 apply (drule_tac P = "\<lambda>a. <id (A) `xb,a>:r" in id_conv [THEN subst],
        assumption)
@@ -194,7 +194,7 @@
 (*Using AC we could trivially prove, for all u, domain(u) \<lesssim> u*)
 lemma lepoll_m_imp_domain_lepoll_m: 
      "\<lbrakk>m \<in> nat; u \<lesssim> m\<rbrakk> \<Longrightarrow> domain(u) \<lesssim> m"
-apply (unfold lepoll_def)
+  unfolding lepoll_def
 apply (erule exE)
 apply (rule_tac x = "\<lambda>x \<in> domain(u). \<mu> i. \<exists>y. \<langle>x,y\<rangle> \<in> u \<and> f`\<langle>x,y\<rangle> = i" 
        in exI)
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/AC/Cardinal_aux.thy
--- a/src/ZF/AC/Cardinal_aux.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/Cardinal_aux.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -99,7 +99,7 @@
 by blast
 
 lemma UN_sing_lepoll: "Ord(a) \<Longrightarrow> (\<Union>x \<in> a. {P(x)}) \<lesssim> a"
-apply (unfold lepoll_def)
+  unfolding lepoll_def
 apply (rule_tac x = "\<lambda>z \<in> (\<Union>x \<in> a. {P (x) }) . (\<mu> i. P (i) =z) " in exI)
 apply (rule_tac d = "\<lambda>z. P (z) " in lam_injective)
 apply (fast intro!: Least_in_Ord)
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/AC/DC.thy
--- a/src/ZF/AC/DC.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/DC.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -9,7 +9,7 @@
 begin
 
 lemma RepFun_lepoll: "Ord(a) \<Longrightarrow> {P(b). b \<in> a} \<lesssim> a"
-apply (unfold lepoll_def)
+  unfolding lepoll_def
 apply (rule_tac x = "\<lambda>z \<in> RepFun (a,P) . \<mu> i. z=P (i) " in exI)
 apply (rule_tac d="\<lambda>z. P (z)" in lam_injective)
  apply (fast intro!: Least_in_Ord)
@@ -19,7 +19,7 @@
 
 text\<open>Trivial in the presence of AC, but here we need a wellordering of X\<close>
 lemma image_Ord_lepoll: "\<lbrakk>f \<in> X->Y; Ord(X)\<rbrakk> \<Longrightarrow> f``X \<lesssim> X"
-apply (unfold lepoll_def)
+  unfolding lepoll_def
 apply (rule_tac x = "\<lambda>x \<in> f``X. \<mu> y. f`y = x" in exI)
 apply (rule_tac d = "\<lambda>z. f`z" in lam_injective)
 apply (fast intro!: Least_in_Ord apply_equality, clarify) 
@@ -34,7 +34,7 @@
 by blast 
 
 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)
+  unfolding succ_def
 apply (fast intro!: fun_extend elim!: mem_irrefl)
 done
 
@@ -352,7 +352,7 @@
 lemma f_n_type:
      "\<lbrakk>domain(f`n) = succ(k); f \<in> nat -> XX;  n \<in> nat\<rbrakk>    
       \<Longrightarrow> f`n \<in> succ(k) -> domain(R)"
-apply (unfold XX_def)
+  unfolding XX_def
 apply (drule apply_type, assumption)
 apply (fast elim: domain_eq_imp_fun_type)
 done
@@ -360,7 +360,7 @@
 lemma f_n_pairs_in_R [rule_format]: 
      "\<lbrakk>h \<in> nat -> XX;  domain(h`n) = succ(k);  n \<in> nat\<rbrakk>   
       \<Longrightarrow> \<forall>i \<in> k. <h`n`i, h`n`succ(i)> \<in> R"
-apply (unfold XX_def)
+  unfolding XX_def
 apply (drule apply_type, assumption)
 apply (elim UN_E CollectE)
 apply (drule domain_of_fun [symmetric, THEN trans], assumption, simp)
@@ -369,7 +369,7 @@
 lemma restrict_cons_eq_restrict: 
      "\<lbrakk>restrict(h, domain(u))=u;  h \<in> n->X;  domain(u) \<subseteq> n\<rbrakk>   
       \<Longrightarrow> restrict(cons(\<langle>n, y\<rangle>, h), domain(u)) = u"
-apply (unfold restrict_def)
+  unfolding restrict_def
 apply (simp add: restrict_def Pi_iff)
 apply (erule sym [THEN trans, symmetric])
 apply (blast elim: mem_irrefl)  
@@ -437,13 +437,13 @@
 lemma lemma2: 
      "\<lbrakk>allRR; f \<in> nat->XX; range(R) \<subseteq> domain(R); x \<in> domain(R); n \<in> nat\<rbrakk>
       \<Longrightarrow> f`n \<in> succ(n) -> domain(R) \<and> (\<forall>i \<in> n. <f`n`i, f`n`succ(i)>:R)"
-apply (unfold allRR_def)
+  unfolding allRR_def
 apply (drule ospec)
 apply (erule ltI [OF _ Ord_nat])
 apply (erule CollectE, simp)
 apply (rule conjI)
 prefer 2 apply (fast elim!: f_n_pairs_in_R trans subst_context)
-apply (unfold XX_def)
+  unfolding XX_def
 apply (fast elim!: trans [THEN domain_eq_imp_fun_type] subst_context)
 done
 
@@ -451,7 +451,7 @@
      "\<lbrakk>allRR; f \<in> nat->XX; n\<in>nat; range(R) \<subseteq> domain(R);  x \<in> domain(R)\<rbrakk>
       \<Longrightarrow> f`n`n = f`succ(n)`n"
 apply (frule lemma2 [THEN conjunct1, THEN domain_of_fun], assumption+)
-apply (unfold allRR_def)
+  unfolding allRR_def
 apply (drule ospec) 
 apply (drule ltI [OF nat_succI Ord_nat], assumption, simp)
 apply (elim conjE ballE)
@@ -497,7 +497,7 @@
 by (fast elim!: image_fun [THEN ssubst])
 
 lemma lesspoll_lemma: "\<lbrakk>\<not> A \<prec> B; C \<prec> B\<rbrakk> \<Longrightarrow> A - C \<noteq> 0"
-apply (unfold lesspoll_def)
+  unfolding lesspoll_def
 apply (fast dest!: Diff_eq_0_iff [THEN iffD1, THEN subset_imp_lepoll]
             intro!: eqpollI elim: notE
             elim!: eqpollE lepoll_trans)
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/AC/HH.thy
--- a/src/ZF/AC/HH.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/HH.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -196,7 +196,7 @@
          f \<in> (Pow(x)-{0}) -> {{z}. z \<in> x}\<rbrakk>   
       \<Longrightarrow> (\<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)
+  unfolding bij_def
 apply (fast intro!: lam_Least_HH_inj lam_surj_sing f_sing_imp_HH_sing)
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/AC/Hartog.thy
--- a/src/ZF/AC/Hartog.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/Hartog.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -20,7 +20,7 @@
 lemma Ord_lepoll_imp_ex_well_ord:
      "\<lbrakk>Ord(a); a \<lesssim> X\<rbrakk> 
       \<Longrightarrow> \<exists>Y. Y \<subseteq> X \<and> (\<exists>R. well_ord(Y,R) \<and> ordertype(Y,R)=a)"
-apply (unfold lepoll_def)
+  unfolding lepoll_def
 apply (erule exE)
 apply (intro exI conjI)
   apply (erule inj_is_fun [THEN fun_is_rel, THEN image_subset])
@@ -60,7 +60,7 @@
 done
 
 lemma not_Hartog_lepoll_self: "\<not> Hartog(A) \<lesssim> A"
-apply (unfold Hartog_def)
+  unfolding Hartog_def
 apply (rule ex_Ord_not_lepoll [THEN exE])
 apply (rule LeastI, auto) 
 done
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/AC/WO1_AC.thy
--- a/src/ZF/AC/WO1_AC.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/WO1_AC.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -40,7 +40,7 @@
 (* ********************************************************************** *)
 
 lemma lemma1: "\<lbrakk>WO1; \<forall>B \<in> A. \<exists>C \<in> D(B). P(C,B)\<rbrakk> \<Longrightarrow> \<exists>f. \<forall>B \<in> A. P(f`B,B)"
-apply (unfold WO1_def)
+  unfolding WO1_def
 apply (erule_tac x = "\<Union>({{C \<in> D (B) . P (C,B) }. B \<in> A}) " in allE)
 apply (erule exE, drule ex_choice_fun, fast)
 apply (erule exE)
@@ -49,7 +49,7 @@
 done
 
 lemma lemma2_1: "\<lbrakk>\<not>Finite(B); WO1\<rbrakk> \<Longrightarrow> |B| + |B| \<approx>  B"
-apply (unfold WO1_def)
+  unfolding WO1_def
 apply (rule eqpoll_trans)
 prefer 2 apply (fast elim!: well_ord_cardinal_eqpoll)
 apply (rule eqpoll_sym [THEN eqpoll_trans])
@@ -67,7 +67,7 @@
 
 lemma lemma2_3: 
         "f \<in> bij(D+D, B) \<Longrightarrow> pairwise_disjoint({{f`Inl(i), f`Inr(i)}. i \<in> D})"
-apply (unfold pairwise_disjoint_def)
+  unfolding pairwise_disjoint_def
 apply (blast dest: bij_is_inj [THEN inj_apply_equality])
 done
 
@@ -98,7 +98,7 @@
 done
 
 theorem WO1_AC10: "\<lbrakk>WO1; 1\<le>n\<rbrakk> \<Longrightarrow> AC10(n)"
-apply (unfold AC10_def)
+  unfolding AC10_def
 apply (fast intro!: lemma1 elim!: lemma2)
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/AC/WO1_WO7.thy
--- a/src/ZF/AC/WO1_WO7.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/WO1_WO7.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -57,7 +57,7 @@
 
 lemma converse_Memrel_not_well_ord: 
     "\<lbrakk>Ord(a); \<not>Finite(a)\<rbrakk> \<Longrightarrow> \<not>well_ord(a,converse(Memrel(a)))"
-apply (unfold well_ord_def)
+  unfolding well_ord_def
 apply (blast dest: converse_Memrel_not_wf_on)
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/AC/WO2_AC16.thy
--- a/src/ZF/AC/WO2_AC16.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/WO2_AC16.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -76,7 +76,7 @@
 
 lemma recfunAC16_mono: 
        "i\<le>j \<Longrightarrow> recfunAC16(f, g, i, a) \<subseteq> recfunAC16(f, g, j, a)"
-apply (unfold recfunAC16_def)
+  unfolding recfunAC16_def
 apply (rule transrec2_mono, auto) 
 done
 
@@ -167,10 +167,10 @@
 
 lemma Finite_lesspoll_infinite_Ord: 
       "\<lbrakk>Finite(X); \<not>Finite(a); Ord(a)\<rbrakk> \<Longrightarrow> X\<prec>a"
-apply (unfold lesspoll_def)
+  unfolding lesspoll_def
 apply (rule conjI)
 apply (drule nat_le_infinite_Ord [THEN le_imp_lepoll], assumption)
-apply (unfold Finite_def)
+  unfolding Finite_def
 apply (blast intro: leI [THEN le_imp_subset, THEN subset_imp_lepoll]
                     ltI eqpoll_imp_lepoll lepoll_trans) 
 apply (blast intro: eqpoll_sym [THEN eqpoll_trans])
@@ -256,7 +256,7 @@
       \<Longrightarrow> (\<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)). \<mu> i. z \<in> F (i) " in exI)
-apply (unfold inj_def)
+  unfolding inj_def
 apply (rule CollectI)
 apply (rule lam_type)
 apply (erule OUN_E)
@@ -547,7 +547,7 @@
 (* ********************************************************************** *)
 
 theorem WO2_AC16: "\<lbrakk>WO2; 0<m; k \<in> nat; m \<in> nat\<rbrakk> \<Longrightarrow> AC16(k #+ m,k)"
-apply (unfold AC16_def)
+  unfolding AC16_def
 apply (rule allI)
 apply (rule impI)
 apply (frule WO2_infinite_subsets_eqpoll_X, assumption+)
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/AC/WO6_WO1.thy
--- a/src/ZF/AC/WO6_WO1.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/AC/WO6_WO1.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -86,7 +86,7 @@
 by (fast intro!: lam_type apply_type)
 
 lemma surj_imp_eq': "f \<in> surj(A,B) \<Longrightarrow> (\<Union>a \<in> A. {f`a}) = B"
-apply (unfold surj_def)
+  unfolding surj_def
 apply (fast elim!: apply_type)
 done
 
@@ -109,7 +109,7 @@
 (* ********************************************************************** *)
 
 lemma WO4_mono: "\<lbrakk>m\<le>n; WO4(m)\<rbrakk> \<Longrightarrow> WO4(n)"
-apply (unfold WO4_def)
+  unfolding WO4_def
 apply (blast dest!: spec intro: lepoll_trans [OF _ le_imp_lepoll])
 done
 
@@ -175,7 +175,7 @@
                   (\<exists>g<a. \<exists>d<a. u(f,b,g,d) \<noteq> 0 \<and> u(f,b,g,d) \<prec> m))  
         | (\<exists>b<a. f`b \<noteq> 0 \<and> (\<forall>g<a. \<forall>d<a. u(f,b,g,d) \<noteq> 0 \<longrightarrow>   
                                         u(f,b,g,d) \<approx> m))"
-apply (unfold lesspoll_def)
+  unfolding lesspoll_def
 apply (blast del: equalityI)
 done
 
@@ -330,7 +330,7 @@
          \<forall>b<a. f`b \<lesssim> succ(m); y*y \<subseteq> y;                        
          (\<Union>b<a. f`b)=y;  Ord(a);  m \<in> nat;  s \<in> f`b;  b<a\<rbrakk> 
       \<Longrightarrow> (\<Union>g<a++a. gg2(f,a,b,s) ` g) = y"
-apply (unfold gg2_def)
+  unfolding gg2_def
 apply (drule sym) 
 apply (simp add: ltD UN_oadd  oadd_le_self [THEN le_imp_not_lt] 
                  lt_Ord odiff_oadd_inverse ww2_def 
@@ -346,7 +346,7 @@
 (* ********************************************************************** *)
 
 lemma vv2_lepoll: "\<lbrakk>m \<in> nat; m\<noteq>0\<rbrakk> \<Longrightarrow> vv2(f,b,g,s) \<lesssim> m"
-apply (unfold vv2_def)
+  unfolding vv2_def
 apply (simp add: empty_lepollI)
 apply (fast dest!: le_imp_subset [THEN subset_imp_lepoll, THEN lepoll_0_is_0] 
        intro!: singleton_eqpoll_1 [THEN eqpoll_imp_lepoll, THEN lepoll_trans]
@@ -357,7 +357,7 @@
 lemma ww2_lepoll: 
     "\<lbrakk>\<forall>b<a. f`b \<lesssim> succ(m);  g<a;  m \<in> nat;  vv2(f,b,g,d) \<subseteq> f`g\<rbrakk>  
      \<Longrightarrow> ww2(f,b,g,d) \<lesssim> m"
-apply (unfold ww2_def)
+  unfolding ww2_def
 apply (case_tac "f`g = 0")
 apply (simp add: empty_lepollI)
 apply (drule ospec, assumption)
@@ -381,7 +381,7 @@
 (* lemma ii                                                               *)
 (* ********************************************************************** *)
 lemma lemma_ii: "\<lbrakk>succ(m) \<in> NN(y); y*y \<subseteq> y; m \<in> nat; m\<noteq>0\<rbrakk> \<Longrightarrow> m \<in> NN(y)"
-apply (unfold NN_def)
+  unfolding NN_def
 apply (elim CollectE exE conjE) 
 apply (rule quant_domain_uu_lepoll_m [THEN cases, THEN disjE], assumption)
 (* case 1 *)
@@ -472,7 +472,7 @@
 done
 
 lemma NN_imp_ex_inj: "1 \<in> NN(y) \<Longrightarrow> \<exists>a f. Ord(a) \<and> f \<in> inj(y, a)"
-apply (unfold NN_def)
+  unfolding NN_def
 apply (elim CollectE exE conjE)
 apply (rule_tac x = a in exI)
 apply (rule_tac x = "\<lambda>x \<in> y. \<mu> i. f`i = {x}" in exI)
@@ -517,12 +517,12 @@
 
 (* another helpful lemma *)
 lemma NN_y_0: "0 \<in> NN(y) \<Longrightarrow> y=0"
-apply (unfold NN_def) 
+  unfolding NN_def 
 apply (fast intro!: equalityI dest!: lepoll_0_is_0 elim: subst)
 done
 
 lemma WO6_imp_WO1: "WO6 \<Longrightarrow> WO1"
-apply (unfold WO1_def)
+  unfolding WO1_def
 apply (rule allI)
 apply (case_tac "A=0")
 apply (fast intro!: well_ord_Memrel nat_0I [THEN nat_into_Ord])
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Arith.thy
--- a/src/ZF/Arith.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Arith.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -191,7 +191,7 @@
 by (simp add: diff_def raw_diff_type)
 
 lemma diff_0_eq_0 [simp]: "0 #- n = 0"
-apply (unfold diff_def)
+  unfolding diff_def
 apply (rule natify_in_nat [THEN nat_induct], auto)
 done
 
@@ -245,7 +245,7 @@
 done
 
 lemma add_succ_right [simp]: "m #+ succ(n) = succ(m #+ n)"
-apply (unfold add_def)
+  unfolding add_def
 apply (rule_tac n = "natify(m) " in nat_induct)
 apply (auto simp add: natify_succ)
 done
@@ -278,7 +278,7 @@
 done
 
 lemma add_left_cancel_natify: "k #+ m = k #+ n \<Longrightarrow> natify(m) = natify(n)"
-apply (unfold add_def)
+  unfolding add_def
 apply (drule raw_add_left_cancel, auto)
 done
 
@@ -468,7 +468,7 @@
 
 (*right annihilation in product*)
 lemma mult_0_right [simp]: "m #* 0 = 0"
-apply (unfold mult_def)
+  unfolding mult_def
 apply (rule_tac n = "natify(m) " in nat_induct)
 apply auto
 done
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/ArithSimp.thy
--- a/src/ZF/ArithSimp.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/ArithSimp.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -82,14 +82,14 @@
     nat_into_Ord not_lt_iff_le [THEN iffD1]
 
 lemma raw_mod_type: "\<lbrakk>m:nat;  n:nat\<rbrakk> \<Longrightarrow> raw_mod (m, n) \<in> nat"
-apply (unfold raw_mod_def)
+  unfolding raw_mod_def
 apply (rule Ord_transrec_type)
 apply (auto simp add: nat_into_Ord [THEN Ord_0_lt_iff])
 apply (blast intro: div_rls)
 done
 
 lemma mod_type [TC,iff]: "m mod n \<in> nat"
-apply (unfold mod_def)
+  unfolding mod_def
 apply (simp (no_asm) add: mod_def raw_mod_type)
 done
 
@@ -98,13 +98,13 @@
     certain equations **)
 
 lemma DIVISION_BY_ZERO_DIV: "a div 0 = 0"
-apply (unfold div_def)
+  unfolding div_def
 apply (rule raw_div_def [THEN def_transrec, THEN trans])
 apply (simp (no_asm_simp))
 done  (*NOT for adding to default simpset*)
 
 lemma DIVISION_BY_ZERO_MOD: "a mod 0 = natify(a)"
-apply (unfold mod_def)
+  unfolding mod_def
 apply (rule raw_mod_def [THEN def_transrec, THEN trans])
 apply (simp (no_asm_simp))
 done  (*NOT for adding to default simpset*)
@@ -138,14 +138,14 @@
 subsection\<open>Division\<close>
 
 lemma raw_div_type: "\<lbrakk>m:nat;  n:nat\<rbrakk> \<Longrightarrow> raw_div (m, n) \<in> nat"
-apply (unfold raw_div_def)
+  unfolding raw_div_def
 apply (rule Ord_transrec_type)
 apply (auto simp add: nat_into_Ord [THEN Ord_0_lt_iff])
 apply (blast intro: div_rls)
 done
 
 lemma div_type [TC,iff]: "m div n \<in> nat"
-apply (unfold div_def)
+  unfolding div_def
 apply (simp (no_asm) add: div_def raw_div_type)
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Bin.thy
--- a/src/ZF/Bin.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Bin.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -164,7 +164,7 @@
 (*This proof is complicated by the mutual recursion*)
 lemma bin_add_type [rule_format]:
      "v \<in> bin \<Longrightarrow> \<forall>w\<in>bin. bin_add(v,w) \<in> bin"
-apply (unfold bin_add_def)
+  unfolding bin_add_def
 apply (induct_tac "v")
 apply (rule_tac [3] ballI)
 apply (rename_tac [3] "w'")
@@ -215,7 +215,7 @@
 by (unfold bin_add_def, simp)
 
 lemma bin_add_Pls_right: "w \<in> bin \<Longrightarrow> bin_add(w,Pls) = w"
-apply (unfold bin_add_def)
+  unfolding bin_add_def
 apply (erule bin.induct, auto)
 done
 
@@ -223,7 +223,7 @@
 by (unfold bin_add_def, simp)
 
 lemma bin_add_Min_right: "w \<in> bin \<Longrightarrow> bin_add(w,Min) = bin_pred(w)"
-apply (unfold bin_add_def)
+  unfolding bin_add_def
 apply (erule bin.induct, auto)
 done
 
@@ -252,7 +252,7 @@
 lemma diff_integ_of_eq:
      "\<lbrakk>v \<in> bin;  w \<in> bin\<rbrakk>
       \<Longrightarrow> integ_of(v) $- integ_of(w) = integ_of(bin_add (v, bin_minus(w)))"
-apply (unfold zdiff_def)
+  unfolding zdiff_def
 apply (simp add: integ_of_add integ_of_minus)
 done
 
@@ -362,7 +362,7 @@
      "\<lbrakk>v \<in> bin;  w \<in> bin\<rbrakk>
       \<Longrightarrow> ((integ_of(v)) = integ_of(w)) \<longleftrightarrow>
           iszero (integ_of (bin_add (v, bin_minus(w))))"
-apply (unfold iszero_def)
+  unfolding iszero_def
 apply (simp add: zcompare_rls integ_of_add integ_of_minus)
 done
 
@@ -371,7 +371,7 @@
 
 
 lemma nonzero_integ_of_Min: "\<not> iszero (integ_of(Min))"
-apply (unfold iszero_def)
+  unfolding iszero_def
 apply (simp add: zminus_equation)
 done
 
@@ -497,7 +497,7 @@
 lemma add_integ_of_diff1 [simp]:
     "\<lbrakk>v \<in> bin;  w \<in> bin\<rbrakk>
       \<Longrightarrow> integ_of(v) $+ (integ_of(w) $- c) = integ_of(bin_add(v,w)) $- (c)"
-apply (unfold zdiff_def)
+  unfolding zdiff_def
 apply (rule add_integ_of_left, auto)
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Cardinal.thy
--- a/src/ZF/Cardinal.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Cardinal.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -79,7 +79,7 @@
 (** Equipollence is an equivalence relation **)
 
 lemma bij_imp_eqpoll: "f \<in> bij(A,B) \<Longrightarrow> A \<approx> B"
-apply (unfold eqpoll_def)
+  unfolding eqpoll_def
 apply (erule exI)
 done
 
@@ -87,20 +87,20 @@
 lemmas eqpoll_refl = id_bij [THEN bij_imp_eqpoll, simp]
 
 lemma eqpoll_sym: "X \<approx> Y \<Longrightarrow> Y \<approx> X"
-apply (unfold eqpoll_def)
+  unfolding eqpoll_def
 apply (blast intro: bij_converse_bij)
 done
 
 lemma eqpoll_trans [trans]:
     "\<lbrakk>X \<approx> Y;  Y \<approx> Z\<rbrakk> \<Longrightarrow> X \<approx> Z"
-apply (unfold eqpoll_def)
+  unfolding eqpoll_def
 apply (blast intro: comp_bij)
 done
 
 (** Le-pollence is a partial ordering **)
 
 lemma subset_imp_lepoll: "X<=Y \<Longrightarrow> X \<lesssim> Y"
-apply (unfold lepoll_def)
+  unfolding lepoll_def
 apply (rule exI)
 apply (erule id_subset_inj)
 done
@@ -113,7 +113,7 @@
 by (unfold eqpoll_def bij_def lepoll_def, blast)
 
 lemma lepoll_trans [trans]: "\<lbrakk>X \<lesssim> Y;  Y \<lesssim> Z\<rbrakk> \<Longrightarrow> X \<lesssim> Z"
-apply (unfold lepoll_def)
+  unfolding lepoll_def
 apply (blast intro: comp_inj)
 done
 
@@ -150,7 +150,7 @@
 
 lemma Un_lepoll_Un:
     "\<lbrakk>A \<lesssim> B; C \<lesssim> D; B \<inter> D = 0\<rbrakk> \<Longrightarrow> A \<union> C \<lesssim> B \<union> D"
-apply (unfold lepoll_def)
+  unfolding lepoll_def
 apply (blast intro: inj_disjoint_Un)
 done
 
@@ -163,7 +163,7 @@
 lemma eqpoll_disjoint_Un:
     "\<lbrakk>A \<approx> B;  C \<approx> D;  A \<inter> C = 0;  B \<inter> D = 0\<rbrakk>
      \<Longrightarrow> A \<union> C \<approx> B \<union> D"
-apply (unfold eqpoll_def)
+  unfolding eqpoll_def
 apply (blast intro: bij_disjoint_Un)
 done
 
@@ -180,12 +180,12 @@
 by (unfold lesspoll_def, blast)
 
 lemma lepoll_well_ord: "\<lbrakk>A \<lesssim> B; well_ord(B,r)\<rbrakk> \<Longrightarrow> \<exists>s. well_ord(A,s)"
-apply (unfold lepoll_def)
+  unfolding lepoll_def
 apply (blast intro: well_ord_rvimage)
 done
 
 lemma lepoll_iff_leqpoll: "A \<lesssim> B \<longleftrightarrow> A \<prec> B | A \<approx> B"
-apply (unfold lesspoll_def)
+  unfolding lesspoll_def
 apply (blast intro!: eqpollI elim!: eqpollE)
 done
 
@@ -208,19 +208,19 @@
 
 lemma lesspoll_trans [trans]:
       "\<lbrakk>X \<prec> Y; Y \<prec> Z\<rbrakk> \<Longrightarrow> X \<prec> Z"
-apply (unfold lesspoll_def)
+  unfolding lesspoll_def
 apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
 done
 
 lemma lesspoll_trans1 [trans]:
       "\<lbrakk>X \<lesssim> Y; Y \<prec> Z\<rbrakk> \<Longrightarrow> X \<prec> Z"
-apply (unfold lesspoll_def)
+  unfolding lesspoll_def
 apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
 done
 
 lemma lesspoll_trans2 [trans]:
       "\<lbrakk>X \<prec> Y; Y \<lesssim> Z\<rbrakk> \<Longrightarrow> X \<prec> Z"
-apply (unfold lesspoll_def)
+  unfolding lesspoll_def
 apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
 done
 
@@ -237,7 +237,7 @@
 
 lemma Least_equality:
     "\<lbrakk>P(i);  Ord(i);  \<And>x. x<i \<Longrightarrow> \<not>P(x)\<rbrakk> \<Longrightarrow> (\<mu> x. P(x)) = i"
-apply (unfold Least_def)
+  unfolding Least_def
 apply (rule the_equality, blast)
 apply (elim conjE)
 apply (erule Ord_linear_lt, assumption, blast+)
@@ -304,7 +304,7 @@
 (*If there is no such P then \<mu> is vacuously 0*)
 lemma Least_0:
     "\<lbrakk>\<not> (\<exists>i. Ord(i) \<and> P(i))\<rbrakk> \<Longrightarrow> (\<mu> x. P(x)) = 0"
-apply (unfold Least_def)
+  unfolding Least_def
 apply (rule the_0, blast)
 done
 
@@ -369,12 +369,12 @@
 (** Observations from Kunen, page 28 **)
 
 lemma Ord_cardinal_le: "Ord(i) \<Longrightarrow> |i| \<le> i"
-apply (unfold cardinal_def)
+  unfolding cardinal_def
 apply (erule eqpoll_refl [THEN Least_le])
 done
 
 lemma Card_cardinal_eq: "Card(K) \<Longrightarrow> |K| = K"
-apply (unfold Card_def)
+  unfolding Card_def
 apply (erule sym)
 done
 
@@ -396,7 +396,7 @@
 done
 
 lemma Ord_cardinal [simp,intro!]: "Ord(|A|)"
-apply (unfold cardinal_def)
+  unfolding cardinal_def
 apply (rule Ord_Least)
 done
 
@@ -417,7 +417,7 @@
 qed
 
 lemma lt_Card_imp_lesspoll: "\<lbrakk>Card(a); i<a\<rbrakk> \<Longrightarrow> i \<prec> a"
-apply (unfold lesspoll_def)
+  unfolding lesspoll_def
 apply (drule Card_iff_initial [THEN iffD1])
 apply (blast intro!: leI [THEN le_imp_lepoll])
 done
@@ -536,7 +536,7 @@
 by (blast intro: lepoll_cardinal_le well_ord_Memrel well_ord_cardinal_eqpoll dest!: lepoll_well_ord)
 
 lemma lesspoll_imp_eqpoll: "\<lbrakk>A \<prec> i; Ord(i)\<rbrakk> \<Longrightarrow> |A| \<approx> A"
-apply (unfold lesspoll_def)
+  unfolding lesspoll_def
 apply (blast intro: lepoll_Ord_imp_eqpoll)
 done
 
@@ -569,7 +569,7 @@
 
 (*Lemma suggested by Mike Fourman*)
 lemma succ_lepoll_succD: "succ(m) \<lesssim> succ(n) \<Longrightarrow> m \<lesssim> n"
-apply (unfold succ_def)
+  unfolding succ_def
 apply (erule cons_lepoll_consD)
 apply (rule mem_not_refl)+
 done
@@ -757,7 +757,7 @@
 by (blast intro: cons_eqpoll_cong cons_eqpoll_consD)
 
 lemma singleton_eqpoll_1: "{a} \<approx> 1"
-apply (unfold succ_def)
+  unfolding succ_def
 apply (blast intro!: eqpoll_refl [THEN cons_eqpoll_cong])
 done
 
@@ -775,26 +775,26 @@
 
 (*Congruence law for  succ  under equipollence*)
 lemma succ_eqpoll_cong: "A \<approx> B \<Longrightarrow> succ(A) \<approx> succ(B)"
-apply (unfold succ_def)
+  unfolding succ_def
 apply (simp add: cons_eqpoll_cong mem_not_refl)
 done
 
 (*Congruence law for + under equipollence*)
 lemma sum_eqpoll_cong: "\<lbrakk>A \<approx> C;  B \<approx> D\<rbrakk> \<Longrightarrow> A+B \<approx> C+D"
-apply (unfold eqpoll_def)
+  unfolding eqpoll_def
 apply (blast intro!: sum_bij)
 done
 
 (*Congruence law for * under equipollence*)
 lemma prod_eqpoll_cong:
     "\<lbrakk>A \<approx> C;  B \<approx> D\<rbrakk> \<Longrightarrow> A*B \<approx> C*D"
-apply (unfold eqpoll_def)
+  unfolding eqpoll_def
 apply (blast intro!: prod_bij)
 done
 
 lemma inj_disjoint_eqpoll:
     "\<lbrakk>f \<in> inj(A,B);  A \<inter> B = 0\<rbrakk> \<Longrightarrow> A \<union> (B - range(f)) \<approx> B"
-apply (unfold eqpoll_def)
+  unfolding eqpoll_def
 apply (rule exI)
 apply (rule_tac c = "\<lambda>x. if x \<in> A then f`x else x"
             and d = "\<lambda>y. if y \<in> range (f) then converse (f) `y else y"
@@ -815,7 +815,7 @@
       then \<^term>\<open>A-{a}\<close> has at most \<^term>\<open>n\<close>.\<close>
 lemma Diff_sing_lepoll:
       "\<lbrakk>a \<in> A;  A \<lesssim> succ(n)\<rbrakk> \<Longrightarrow> A - {a} \<lesssim> n"
-apply (unfold succ_def)
+  unfolding succ_def
 apply (rule cons_lepoll_consD)
 apply (rule_tac [3] mem_not_refl)
 apply (erule cons_Diff [THEN ssubst], safe)
@@ -846,7 +846,7 @@
 done
 
 lemma Un_lepoll_sum: "A \<union> B \<lesssim> A+B"
-apply (unfold lepoll_def)
+  unfolding lepoll_def
 apply (rule_tac x = "\<lambda>x\<in>A \<union> B. if x\<in>A then Inl (x) else Inr (x)" in exI)
 apply (rule_tac d = "\<lambda>z. snd (z)" in lam_injective)
 apply force
@@ -860,7 +860,7 @@
 
 (*Krzysztof Grabczewski*)
 lemma disj_Un_eqpoll_sum: "A \<inter> B = 0 \<Longrightarrow> A \<union> B \<approx> A + B"
-apply (unfold eqpoll_def)
+  unfolding eqpoll_def
 apply (rule_tac x = "\<lambda>a\<in>A \<union> B. if a \<in> A then Inl (a) else Inr (a)" in exI)
 apply (rule_tac d = "\<lambda>z. case (\<lambda>x. x, \<lambda>x. x, z)" in lam_bijective)
 apply auto
@@ -870,17 +870,17 @@
 subsection \<open>Finite and infinite sets\<close>
 
 lemma eqpoll_imp_Finite_iff: "A \<approx> B \<Longrightarrow> Finite(A) \<longleftrightarrow> Finite(B)"
-apply (unfold Finite_def)
+  unfolding Finite_def
 apply (blast intro: eqpoll_trans eqpoll_sym)
 done
 
 lemma Finite_0 [simp]: "Finite(0)"
-apply (unfold Finite_def)
+  unfolding Finite_def
 apply (blast intro!: eqpoll_refl nat_0I)
 done
 
 lemma Finite_cons: "Finite(x) \<Longrightarrow> Finite(cons(y,x))"
-apply (unfold Finite_def)
+  unfolding Finite_def
 apply (case_tac "y \<in> x")
 apply (simp add: cons_absorb)
 apply (erule bexE)
@@ -890,7 +890,7 @@
 done
 
 lemma Finite_succ: "Finite(x) \<Longrightarrow> Finite(succ(x))"
-apply (unfold succ_def)
+  unfolding succ_def
 apply (erule Finite_cons)
 done
 
@@ -912,7 +912,7 @@
 
 lemma lesspoll_nat_is_Finite:
      "A \<prec> nat \<Longrightarrow> Finite(A)"
-apply (unfold Finite_def)
+  unfolding Finite_def
 apply (blast dest: ltD lesspoll_cardinal_lt
                    lesspoll_imp_eqpoll [THEN eqpoll_sym])
 done
@@ -943,7 +943,7 @@
 
 lemma nat_le_infinite_Ord:
       "\<lbrakk>Ord(i);  \<not> Finite(i)\<rbrakk> \<Longrightarrow> nat \<le> i"
-apply (unfold Finite_def)
+  unfolding Finite_def
 apply (erule Ord_nat [THEN [2] Ord_linear2])
 prefer 2 apply assumption
 apply (blast intro!: eqpoll_refl elim!: ltE)
@@ -993,12 +993,12 @@
 apply (rule Fin.consI, blast)
 apply (blast intro: subset_consI [THEN Fin_mono, THEN subsetD])
 (*Now for the lemma assumed above*)
-apply (unfold eqpoll_def)
+  unfolding eqpoll_def
 apply (blast intro: bij_converse_bij [THEN bij_is_fun, THEN apply_type])
 done
 
 lemma Finite_into_Fin: "Finite(A) \<Longrightarrow> A \<in> Fin(A)"
-apply (unfold Finite_def)
+  unfolding Finite_def
 apply (blast intro: Fin_lemma)
 done
 
@@ -1036,7 +1036,7 @@
 
 (*Sidi Ehmety.  The contrapositive says \<not>Finite(A) \<Longrightarrow> \<not>Finite(A-{a}) *)
 lemma Diff_sing_Finite: "Finite(A - {a}) \<Longrightarrow> Finite(A)"
-apply (unfold Finite_def)
+  unfolding Finite_def
 apply (case_tac "a \<in> A")
 apply (subgoal_tac [2] "A-{a}=A", auto)
 apply (rule_tac x = "succ (n) " in bexI)
@@ -1154,7 +1154,7 @@
 
 lemma Finite_well_ord_converse:
     "\<lbrakk>Finite(A);  well_ord(A,r)\<rbrakk> \<Longrightarrow> well_ord(A,converse(r))"
-apply (unfold Finite_def)
+  unfolding Finite_def
 apply (rule well_ord_converse, assumption)
 apply (blast dest: ordertype_eq_n intro!: nat_well_ord_converse_Memrel)
 done
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/CardinalArith.thy
--- a/src/ZF/CardinalArith.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/CardinalArith.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -73,7 +73,7 @@
   by (auto simp add: OUnion_def Card_0)
 
 lemma in_Card_imp_lesspoll: "\<lbrakk>Card(K); b \<in> K\<rbrakk> \<Longrightarrow> b \<prec> K"
-apply (unfold lesspoll_def)
+  unfolding lesspoll_def
 apply (simp add: Card_iff_initial)
 apply (fast intro!: le_imp_lepoll ltI leI)
 done
@@ -95,14 +95,14 @@
 qed
 
 lemma cadd_commute: "i \<oplus> j = j \<oplus> i"
-apply (unfold cadd_def)
+  unfolding cadd_def
 apply (rule sum_commute_eqpoll [THEN cardinal_cong])
 done
 
 subsubsection\<open>Cardinal addition is associative\<close>
 
 lemma sum_assoc_eqpoll: "(A+B)+C \<approx> A+(B+C)"
-apply (unfold eqpoll_def)
+  unfolding eqpoll_def
 apply (rule exI)
 apply (rule sum_assoc_bij)
 done
@@ -125,13 +125,13 @@
 subsubsection\<open>0 is the identity for addition\<close>
 
 lemma sum_0_eqpoll: "0+A \<approx> A"
-apply (unfold eqpoll_def)
+  unfolding eqpoll_def
 apply (rule exI)
 apply (rule bij_0_sum)
 done
 
 lemma cadd_0 [simp]: "Card(K) \<Longrightarrow> 0 \<oplus> K = K"
-apply (unfold cadd_def)
+  unfolding cadd_def
 apply (simp add: sum_0_eqpoll [THEN cardinal_cong] Card_cardinal_eq)
 done
 
@@ -161,7 +161,7 @@
 
 lemma sum_lepoll_mono:
      "\<lbrakk>A \<lesssim> C;  B \<lesssim> D\<rbrakk> \<Longrightarrow> A + B \<lesssim> C + D"
-apply (unfold lepoll_def)
+  unfolding lepoll_def
 apply (elim exE)
 apply (rule_tac x = "\<lambda>z\<in>A+B. case (\<lambda>w. Inl(f`w), \<lambda>y. Inr(fa`y), z)" in exI)
 apply (rule_tac d = "case (\<lambda>w. Inl(converse(f) `w), \<lambda>y. Inr(converse(fa) ` y))"
@@ -171,7 +171,7 @@
 
 lemma cadd_le_mono:
     "\<lbrakk>K' \<le> K;  L' \<le> L\<rbrakk> \<Longrightarrow> (K' \<oplus> L') \<le> (K \<oplus> L)"
-apply (unfold cadd_def)
+  unfolding cadd_def
 apply (safe dest!: le_subset_iff [THEN iffD1])
 apply (rule well_ord_lepoll_imp_cardinal_le)
 apply (blast intro: well_ord_radd well_ord_Memrel)
@@ -181,7 +181,7 @@
 subsubsection\<open>Addition of finite cardinals is "ordinary" addition\<close>
 
 lemma sum_succ_eqpoll: "succ(A)+B \<approx> succ(A+B)"
-apply (unfold eqpoll_def)
+  unfolding eqpoll_def
 apply (rule exI)
 apply (rule_tac c = "\<lambda>z. if z=Inl (A) then A+B else z"
             and d = "\<lambda>z. if z=A+B then Inl (A) else z" in lam_bijective)
@@ -219,21 +219,21 @@
 subsubsection\<open>Cardinal multiplication is commutative\<close>
 
 lemma prod_commute_eqpoll: "A*B \<approx> B*A"
-apply (unfold eqpoll_def)
+  unfolding eqpoll_def
 apply (rule exI)
 apply (rule_tac c = "\<lambda>\<langle>x,y\<rangle>.\<langle>y,x\<rangle>" and d = "\<lambda>\<langle>x,y\<rangle>.\<langle>y,x\<rangle>" in lam_bijective,
        auto)
 done
 
 lemma cmult_commute: "i \<otimes> j = j \<otimes> i"
-apply (unfold cmult_def)
+  unfolding cmult_def
 apply (rule prod_commute_eqpoll [THEN cardinal_cong])
 done
 
 subsubsection\<open>Cardinal multiplication is associative\<close>
 
 lemma prod_assoc_eqpoll: "(A*B)*C \<approx> A*(B*C)"
-apply (unfold eqpoll_def)
+  unfolding eqpoll_def
 apply (rule exI)
 apply (rule prod_assoc_bij)
 done
@@ -255,7 +255,7 @@
 subsubsection\<open>Cardinal multiplication distributes over addition\<close>
 
 lemma sum_prod_distrib_eqpoll: "(A+B)*C \<approx> (A*C)+(B*C)"
-apply (unfold eqpoll_def)
+  unfolding eqpoll_def
 apply (rule exI)
 apply (rule sum_prod_distrib_bij)
 done
@@ -276,7 +276,7 @@
 subsubsection\<open>Multiplication by 0 yields 0\<close>
 
 lemma prod_0_eqpoll: "0*A \<approx> 0"
-apply (unfold eqpoll_def)
+  unfolding eqpoll_def
 apply (rule exI)
 apply (rule lam_bijective, safe)
 done
@@ -287,7 +287,7 @@
 subsubsection\<open>1 is the identity for multiplication\<close>
 
 lemma prod_singleton_eqpoll: "{x}*A \<approx> A"
-apply (unfold eqpoll_def)
+  unfolding eqpoll_def
 apply (rule exI)
 apply (rule singleton_prod_bij [THEN bij_converse_bij])
 done
@@ -306,7 +306,7 @@
 
 (*Could probably weaken the premise to well_ord(K,r), or remove using AC*)
 lemma cmult_square_le: "Card(K) \<Longrightarrow> K \<le> K \<otimes> K"
-apply (unfold cmult_def)
+  unfolding cmult_def
 apply (rule le_trans)
 apply (rule_tac [2] well_ord_lepoll_imp_cardinal_le)
 apply (rule_tac [3] prod_square_lepoll)
@@ -324,7 +324,7 @@
 (*Could probably weaken the premises to well_ord(K,r), or removing using AC*)
 lemma cmult_le_self:
     "\<lbrakk>Card(K);  Ord(L);  0<L\<rbrakk> \<Longrightarrow> K \<le> (K \<otimes> L)"
-apply (unfold cmult_def)
+  unfolding cmult_def
 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)
@@ -335,7 +335,7 @@
 
 lemma prod_lepoll_mono:
      "\<lbrakk>A \<lesssim> C;  B \<lesssim> D\<rbrakk> \<Longrightarrow> A * B  \<lesssim>  C * D"
-apply (unfold lepoll_def)
+  unfolding lepoll_def
 apply (elim exE)
 apply (rule_tac x = "lam \<langle>w,y\<rangle>:A*B. <f`w, fa`y>" in exI)
 apply (rule_tac d = "\<lambda>\<langle>w,y\<rangle>. <converse (f) `w, converse (fa) `y>"
@@ -345,7 +345,7 @@
 
 lemma cmult_le_mono:
     "\<lbrakk>K' \<le> K;  L' \<le> L\<rbrakk> \<Longrightarrow> (K' \<otimes> L') \<le> (K \<otimes> L)"
-apply (unfold cmult_def)
+  unfolding cmult_def
 apply (safe dest!: le_subset_iff [THEN iffD1])
 apply (rule well_ord_lepoll_imp_cardinal_le)
  apply (blast intro: well_ord_rmult well_ord_Memrel)
@@ -355,7 +355,7 @@
 subsection\<open>Multiplication of finite cardinals is "ordinary" multiplication\<close>
 
 lemma prod_succ_eqpoll: "succ(A)*B \<approx> B + A*B"
-apply (unfold eqpoll_def)
+  unfolding eqpoll_def
 apply (rule exI)
 apply (rule_tac c = "\<lambda>\<langle>x,y\<rangle>. if x=A then Inl (y) else Inr (\<langle>x,y\<rangle>)"
             and d = "case (\<lambda>y. \<langle>A,y\<rangle>, \<lambda>z. z)" in lam_bijective)
@@ -402,7 +402,7 @@
   and inverse \<lambda>y. if y \<in> nat then nat_case(u, \<lambda>z. z, y) else y.  \
   If f \<in> inj(nat,A) then range(f) behaves like the natural numbers.*)
 lemma nat_cons_lepoll: "nat \<lesssim> A \<Longrightarrow> cons(u,A) \<lesssim> A"
-apply (unfold lepoll_def)
+  unfolding lepoll_def
 apply (erule exE)
 apply (rule_tac x =
           "\<lambda>z\<in>cons (u,A).
@@ -426,35 +426,35 @@
 
 (*Specialized version required below*)
 lemma nat_succ_eqpoll: "nat \<subseteq> A \<Longrightarrow> succ(A) \<approx> A"
-apply (unfold succ_def)
+  unfolding succ_def
 apply (erule subset_imp_lepoll [THEN nat_cons_eqpoll])
 done
 
 lemma InfCard_nat: "InfCard(nat)"
-apply (unfold InfCard_def)
+  unfolding InfCard_def
 apply (blast intro: Card_nat le_refl Card_is_Ord)
 done
 
 lemma InfCard_is_Card: "InfCard(K) \<Longrightarrow> Card(K)"
-apply (unfold InfCard_def)
+  unfolding InfCard_def
 apply (erule conjunct1)
 done
 
 lemma InfCard_Un:
     "\<lbrakk>InfCard(K);  Card(L)\<rbrakk> \<Longrightarrow> InfCard(K \<union> L)"
-apply (unfold InfCard_def)
+  unfolding InfCard_def
 apply (simp add: Card_Un Un_upper1_le [THEN [2] le_trans]  Card_is_Ord)
 done
 
 (*Kunen's Lemma 10.11*)
 lemma InfCard_is_Limit: "InfCard(K) \<Longrightarrow> Limit(K)"
-apply (unfold InfCard_def)
+  unfolding InfCard_def
 apply (erule conjE)
 apply (frule Card_is_Ord)
 apply (rule ltI [THEN non_succ_LimitI])
 apply (erule le_imp_subset [THEN subsetD])
 apply (safe dest!: Limit_nat [THEN Limit_le_succD])
-apply (unfold Card_def)
+  unfolding Card_def
 apply (drule trans)
 apply (erule le_imp_subset [THEN nat_succ_eqpoll, THEN cardinal_cong])
 apply (erule Ord_cardinal_le [THEN lt_trans2, THEN lt_irrefl])
@@ -468,7 +468,7 @@
 (*A general fact about ordermap*)
 lemma ordermap_eqpoll_pred:
     "\<lbrakk>well_ord(A,r);  x \<in> A\<rbrakk> \<Longrightarrow> ordermap(A,r)`x \<approx> Order.pred(A,x,r)"
-apply (unfold eqpoll_def)
+  unfolding eqpoll_def
 apply (rule exI)
 apply (simp add: ordermap_eq_image well_ord_is_wf)
 apply (erule ordermap_bij [THEN bij_is_inj, THEN restrict_bij,
@@ -492,7 +492,7 @@
 
 lemma csquareD:
  "\<lbrakk><\<langle>x,y\<rangle>, \<langle>z,z\<rangle>> \<in> csquare_rel(K);  x<K;  y<K;  z<K\<rbrakk> \<Longrightarrow> x \<le> z \<and> y \<le> z"
-apply (unfold csquare_rel_def)
+  unfolding csquare_rel_def
 apply (erule rev_mp)
 apply (elim ltE)
 apply (simp add: rvimage_iff Un_absorb Un_least_mem_iff ltD)
@@ -509,7 +509,7 @@
 
 lemma csquare_ltI:
  "\<lbrakk>x<z;  y<z;  z<K\<rbrakk> \<Longrightarrow>  <\<langle>x,y\<rangle>, \<langle>z,z\<rangle>> \<in> csquare_rel(K)"
-apply (unfold csquare_rel_def)
+  unfolding csquare_rel_def
 apply (subgoal_tac "x<K \<and> y<K")
  prefer 2 apply (blast intro: lt_trans)
 apply (elim ltE)
@@ -519,7 +519,7 @@
 (*Part of the traditional proof.  UNUSED since it's harder to prove \<and> apply *)
 lemma csquare_or_eqI:
  "\<lbrakk>x \<le> z;  y \<le> z;  z<K\<rbrakk> \<Longrightarrow> <\<langle>x,y\<rangle>, \<langle>z,z\<rangle>> \<in> csquare_rel(K) | x=z \<and> y=z"
-apply (unfold csquare_rel_def)
+  unfolding csquare_rel_def
 apply (subgoal_tac "x<K \<and> y<K")
  prefer 2 apply (blast intro: lt_trans1)
 apply (elim ltE)
@@ -731,10 +731,10 @@
 text\<open>This result is Kunen's Theorem 10.16, which would be trivial using AC\<close>
 
 lemma Ord_jump_cardinal: "Ord(jump_cardinal(K))"
-apply (unfold jump_cardinal_def)
+  unfolding jump_cardinal_def
 apply (rule Ord_is_Transset [THEN [2] OrdI])
  prefer 2 apply (blast intro!: Ord_ordertype)
-apply (unfold Transset_def)
+  unfolding Transset_def
 apply (safe del: subsetI)
 apply (simp add: ordertype_pred_unfold, safe)
 apply (rule UN_I)
@@ -746,7 +746,7 @@
 lemma jump_cardinal_iff:
      "i \<in> jump_cardinal(K) \<longleftrightarrow>
       (\<exists>r X. r \<subseteq> K*K \<and> X \<subseteq> K \<and> well_ord(X,r) \<and> i = ordertype(X,r))"
-apply (unfold jump_cardinal_def)
+  unfolding jump_cardinal_def
 apply (blast del: subsetI)
 done
 
@@ -780,7 +780,7 @@
 (*The hard part of Theorem 10.16: jump_cardinal(K) is itself a cardinal*)
 lemma Card_jump_cardinal: "Card(jump_cardinal(K))"
 apply (rule Ord_jump_cardinal [THEN CardI])
-apply (unfold eqpoll_def)
+  unfolding eqpoll_def
 apply (safe dest!: ltD jump_cardinal_iff [THEN iffD1])
 apply (blast intro: Card_jump_cardinal_lemma [THEN mem_irrefl])
 done
@@ -788,7 +788,7 @@
 subsection\<open>Basic Properties of Successor Cardinals\<close>
 
 lemma csucc_basic: "Ord(K) \<Longrightarrow> Card(csucc(K)) \<and> K < csucc(K)"
-apply (unfold csucc_def)
+  unfolding csucc_def
 apply (rule LeastI)
 apply (blast intro: Card_jump_cardinal K_lt_jump_cardinal Ord_jump_cardinal)+
 done
@@ -801,7 +801,7 @@
 by (blast intro: Ord_0_le lt_csucc lt_trans1)
 
 lemma csucc_le: "\<lbrakk>Card(L);  K<L\<rbrakk> \<Longrightarrow> csucc(K) \<le> L"
-apply (unfold csucc_def)
+  unfolding csucc_def
 apply (rule Least_le)
 apply (blast intro: Card_is_Ord)+
 done
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Coind/ECR.thy
--- a/src/ZF/Coind/ECR.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Coind/ECR.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -98,7 +98,7 @@
       v_clos(x,e,ve_owr(ve,f,cl)) = cl;                           
       hastyenv(ve,te); <te,e_fix(f,x,e),t> \<in> ElabRel\<rbrakk> \<Longrightarrow>        
    \<langle>cl,t\<rangle> \<in> HasTyRel"
-apply (unfold hastyenv_def)
+  unfolding hastyenv_def
 apply (erule elab_fixE, safe)
 apply hypsubst_thin
 apply (rule subst, assumption) 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Coind/Map.thy
--- a/src/ZF/Coind/Map.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Coind/Map.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -69,7 +69,7 @@
 
 lemma MapQU_lemma: 
     "A \<subseteq> univ(X) \<Longrightarrow> Pow(A * \<Union>(quniv(X))) \<subseteq> quniv(X)"
-apply (unfold quniv_def)
+  unfolding quniv_def
 apply (rule Pow_mono)
 apply (rule subset_trans [OF Sigma_mono product_univ])
 apply (erule subset_trans)
@@ -127,7 +127,7 @@
 
 lemma pmap_appI: 
   "\<lbrakk>m \<in> PMap(A,B); a \<in> domain(m)\<rbrakk> \<Longrightarrow> map_app(m,a):B"
-apply (unfold PMap_def)
+  unfolding PMap_def
 apply (frule tmap_app_notempty, assumption)
 apply (drule tmap_appI, auto)
 done
@@ -165,7 +165,7 @@
 
 lemma map_domain_owr: 
   "b \<noteq> 0 \<Longrightarrow> domain(map_owr(f,a,b)) = {a} \<union> domain(f)"
-apply (unfold map_owr_def)
+  unfolding map_owr_def
 apply (auto simp add: domain_Sigma)
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Coind/Values.thy
--- a/src/ZF/Coind/Values.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Coind/Values.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -101,7 +101,7 @@
 done
 
 lemma ve_empI: "ve_emp \<in> ValEnv"
-apply (unfold ve_emp_def)
+  unfolding ve_emp_def
 apply (rule Val_ValEnv.intros)
 apply (rule pmap_empI)
 done
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Constructible/AC_in_L.thy
--- a/src/ZF/Constructible/AC_in_L.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Constructible/AC_in_L.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -216,7 +216,7 @@
 text\<open>Not needed--but interesting?\<close>
 theorem formula_lepoll_nat: "formula \<lesssim> nat"
 apply (insert nat_times_nat_lepoll_nat)
-apply (unfold lepoll_def)
+  unfolding lepoll_def
 apply (blast intro: Nat_Times_Nat.inj_formula_nat Nat_Times_Nat.intro)
 done
 
@@ -447,7 +447,7 @@
 lemma well_ord_L_r:
     "Ord(i) \<Longrightarrow> \<exists>r. well_ord(Lset(i), r)"
 apply (insert nat_times_nat_lepoll_nat)
-apply (unfold lepoll_def)
+  unfolding lepoll_def
 apply (blast intro: Nat_Times_Nat.well_ord_L_r Nat_Times_Nat.intro)
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Constructible/DPow_absolute.thy
--- a/src/ZF/Constructible/DPow_absolute.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Constructible/DPow_absolute.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -177,7 +177,7 @@
 theorem DPow_sats_reflection:
      "REFLECTS[\<lambda>x. is_DPow_sats(L,f(x),g(x),h(x),g'(x)),
                \<lambda>i x. is_DPow_sats(##Lset(i),f(x),g(x),h(x),g'(x))]"
-apply (unfold is_DPow_sats_def) 
+  unfolding is_DPow_sats_def 
 apply (intro FOL_reflections function_reflections extra_reflections
              satisfies_reflection)
 done
@@ -264,7 +264,7 @@
                mem_formula(##Lset(i),p) \<and> mem_list(##Lset(i),A,env) \<and> 
                pair(##Lset(i),env,p,u) \<and>
                is_Collect (##Lset(i), A, is_DPow_sats(##Lset(i),A,env,p), x))]"
-apply (unfold is_Collect_def) 
+  unfolding is_Collect_def 
 apply (intro FOL_reflections function_reflections mem_formula_reflection
           mem_list_reflection DPow_sats_reflection)
 done
@@ -279,7 +279,7 @@
 apply (rule_tac u="{A,B}" 
          in gen_separation_multi [OF DPow_replacement_Reflects], 
        auto)
-apply (unfold is_Collect_def) 
+  unfolding is_Collect_def 
 apply (rule_tac env="[A,B]" in DPow_LsetI)
 apply (rule sep_rules mem_formula_iff_sats mem_list_iff_sats 
             DPow_sats_iff_sats | simp)+
@@ -543,7 +543,7 @@
 
 lemma strong_rep:
    "\<lbrakk>L(x); L(g)\<rbrakk> \<Longrightarrow> strong_replacement(L, \<lambda>y z. transrec_body(L,g,x,y,z))"
-apply (unfold transrec_body_def)  
+  unfolding transrec_body_def  
 apply (rule strong_replacementI) 
 apply (rule_tac u="{x,g,B}" 
          in gen_separation_multi [OF strong_rep_Reflects], auto)
@@ -582,7 +582,7 @@
               \<exists>r[L]. is_Replace(L, x, transrec_body(L,f,x), r) \<and> 
                      big_union(L, r, u), j)"
 apply (rule L.transrec_replacementI, assumption)
-apply (unfold transrec_body_def)  
+  unfolding transrec_body_def  
 apply (rule strong_replacementI)
 apply (rule_tac u="{j,B,Memrel(eclose({j}))}" 
          in gen_separation_multi [OF transrec_rep_Reflects], auto)
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Constructible/Formula.thy
--- a/src/ZF/Constructible/Formula.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Constructible/Formula.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -799,7 +799,7 @@
 
 lemma Pair_in_Lset:
     "\<lbrakk>a \<in> Lset(i);  b \<in> Lset(i); Ord(i)\<rbrakk> \<Longrightarrow> \<langle>a,b\<rangle> \<in> Lset(succ(succ(i)))"
-apply (unfold Pair_def)
+  unfolding Pair_def
 apply (blast intro: doubleton_in_Lset)
 done
 
@@ -862,7 +862,7 @@
 lemma Lset_iff_lrank_lt: "Ord(i) \<Longrightarrow> x \<in> Lset(i) \<longleftrightarrow> L(x) \<and> lrank(x) < i"
 apply (simp add: L_def, auto)
  apply (blast intro: Lset_lrank_lt)
- apply (unfold lrank_def)
+   unfolding lrank_def
 apply (drule succI1 [THEN Lset_mono_mem, THEN subsetD])
 apply (drule_tac P="\<lambda>i. x \<in> Lset(succ(i))" in LeastI, assumption)
 apply (blast intro!: le_imp_subset Lset_mono [THEN subsetD])
@@ -873,7 +873,7 @@
 
 text\<open>Kunen's VI 1.9 (a)\<close>
 lemma lrank_of_Ord: "Ord(i) \<Longrightarrow> lrank(i) = i"
-apply (unfold lrank_def)
+  unfolding lrank_def
 apply (rule Least_equality)
   apply (erule Ord_in_Lset)
  apply assumption
@@ -894,7 +894,7 @@
 done
 
 lemma lrank_Lset: "Ord(i) \<Longrightarrow> lrank(Lset(i)) = i"
-apply (unfold lrank_def)
+  unfolding lrank_def
 apply (rule Least_equality)
   apply (rule Lset_in_Lset_succ)
  apply assumption
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Constructible/L_axioms.thy
--- a/src/ZF/Constructible/L_axioms.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Constructible/L_axioms.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -155,7 +155,7 @@
 
 theorem Not_reflection:
      "REFLECTS[P,Q] \<Longrightarrow> REFLECTS[\<lambda>x. \<not>P(x), \<lambda>a x. \<not>Q(a,x)]"
-apply (unfold L_Reflects_def)
+  unfolding L_Reflects_def
 apply (erule meta_exE)
 apply (rule_tac x=Cl in meta_exI, simp)
 done
@@ -163,7 +163,7 @@
 theorem And_reflection:
      "\<lbrakk>REFLECTS[P,Q]; REFLECTS[P',Q']\<rbrakk>
       \<Longrightarrow> REFLECTS[\<lambda>x. P(x) \<and> P'(x), \<lambda>a x. Q(a,x) \<and> Q'(a,x)]"
-apply (unfold L_Reflects_def)
+  unfolding L_Reflects_def
 apply (elim meta_exE)
 apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI)
 apply (simp add: Closed_Unbounded_Int, blast)
@@ -172,7 +172,7 @@
 theorem Or_reflection:
      "\<lbrakk>REFLECTS[P,Q]; REFLECTS[P',Q']\<rbrakk>
       \<Longrightarrow> REFLECTS[\<lambda>x. P(x) \<or> P'(x), \<lambda>a x. Q(a,x) \<or> Q'(a,x)]"
-apply (unfold L_Reflects_def)
+  unfolding L_Reflects_def
 apply (elim meta_exE)
 apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI)
 apply (simp add: Closed_Unbounded_Int, blast)
@@ -181,7 +181,7 @@
 theorem Imp_reflection:
      "\<lbrakk>REFLECTS[P,Q]; REFLECTS[P',Q']\<rbrakk>
       \<Longrightarrow> REFLECTS[\<lambda>x. P(x) \<longrightarrow> P'(x), \<lambda>a x. Q(a,x) \<longrightarrow> Q'(a,x)]"
-apply (unfold L_Reflects_def)
+  unfolding L_Reflects_def
 apply (elim meta_exE)
 apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI)
 apply (simp add: Closed_Unbounded_Int, blast)
@@ -190,7 +190,7 @@
 theorem Iff_reflection:
      "\<lbrakk>REFLECTS[P,Q]; REFLECTS[P',Q']\<rbrakk>
       \<Longrightarrow> REFLECTS[\<lambda>x. P(x) \<longleftrightarrow> P'(x), \<lambda>a x. Q(a,x) \<longleftrightarrow> Q'(a,x)]"
-apply (unfold L_Reflects_def)
+  unfolding L_Reflects_def
 apply (elim meta_exE)
 apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI)
 apply (simp add: Closed_Unbounded_Int, blast)
@@ -223,14 +223,14 @@
 theorem Rex_reflection:
      "REFLECTS[ \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
       \<Longrightarrow> REFLECTS[\<lambda>x. \<exists>z[L]. P(x,z), \<lambda>a x. \<exists>z\<in>Lset(a). Q(a,x,z)]"
-apply (unfold rex_def)
+  unfolding rex_def
 apply (intro And_reflection Ex_reflection, assumption)
 done
 
 theorem Rall_reflection:
      "REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))]
       \<Longrightarrow> REFLECTS[\<lambda>x. \<forall>z[L]. P(x,z), \<lambda>a x. \<forall>z\<in>Lset(a). Q(a,x,z)]"
-apply (unfold rall_def)
+  unfolding rall_def
 apply (intro Imp_reflection All_reflection, assumption)
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Constructible/Normal.thy
--- a/src/ZF/Constructible/Normal.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Constructible/Normal.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -171,7 +171,7 @@
   done
 
 lemma Unbounded_INT: "Unbounded(\<lambda>x. \<forall>a\<in>A. P(a,x))"
-  apply (unfold Unbounded_def)  
+    unfolding Unbounded_def  
   apply (blast intro!: omega_sup_greater_gt P_omega_sup_greater) 
   done
 
@@ -367,7 +367,7 @@
 
 lemma iterates_omega_increasing:
      "\<lbrakk>Normal(F); Ord(a)\<rbrakk> \<Longrightarrow> a \<le> F^\<omega> (a)"   
-apply (unfold iterates_omega_def)
+  unfolding iterates_omega_def
 apply (rule UN_upper_le [of 0], simp_all)
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Constructible/Satisfies_absolute.thy
--- a/src/ZF/Constructible/Satisfies_absolute.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Constructible/Satisfies_absolute.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -595,7 +595,7 @@
 theorem satisfies_is_a_reflection:
      "REFLECTS[\<lambda>x. satisfies_is_a(L,f(x),g(x),h(x),g'(x)),
                \<lambda>i x. satisfies_is_a(##Lset(i),f(x),g(x),h(x),g'(x))]"
-apply (unfold satisfies_is_a_def) 
+  unfolding satisfies_is_a_def 
 apply (intro FOL_reflections is_lambda_reflection bool_of_o_reflection 
              nth_reflection is_list_reflection)
 done
@@ -644,7 +644,7 @@
 theorem satisfies_is_b_reflection:
      "REFLECTS[\<lambda>x. satisfies_is_b(L,f(x),g(x),h(x),g'(x)),
                \<lambda>i x. satisfies_is_b(##Lset(i),f(x),g(x),h(x),g'(x))]"
-apply (unfold satisfies_is_b_def) 
+  unfolding satisfies_is_b_def 
 apply (intro FOL_reflections is_lambda_reflection bool_of_o_reflection 
              nth_reflection is_list_reflection)
 done
@@ -695,7 +695,7 @@
 theorem satisfies_is_c_reflection:
      "REFLECTS[\<lambda>x. satisfies_is_c(L,f(x),g(x),h(x),g'(x),h'(x)),
                \<lambda>i x. satisfies_is_c(##Lset(i),f(x),g(x),h(x),g'(x),h'(x))]"
-apply (unfold satisfies_is_c_def) 
+  unfolding satisfies_is_c_def 
 apply (intro FOL_reflections function_reflections is_lambda_reflection
              extra_reflections nth_reflection depth_apply_reflection 
              is_list_reflection)
@@ -751,7 +751,7 @@
 theorem satisfies_is_d_reflection:
      "REFLECTS[\<lambda>x. satisfies_is_d(L,f(x),g(x),h(x),g'(x)),
                \<lambda>i x. satisfies_is_d(##Lset(i),f(x),g(x),h(x),g'(x))]"
-apply (unfold satisfies_is_d_def) 
+  unfolding satisfies_is_d_def 
 apply (intro FOL_reflections function_reflections is_lambda_reflection
              extra_reflections nth_reflection depth_apply_reflection 
              is_list_reflection)
@@ -810,7 +810,7 @@
 theorem satisfies_MH_reflection:
      "REFLECTS[\<lambda>x. satisfies_MH(L,f(x),g(x),h(x),g'(x)),
                \<lambda>i x. satisfies_MH(##Lset(i),f(x),g(x),h(x),g'(x))]"
-apply (unfold satisfies_MH_def) 
+  unfolding satisfies_MH_def 
 apply (intro FOL_reflections satisfies_reflections)
 done
 
@@ -925,7 +925,7 @@
             is_Cons(##Lset(i),a,u,co) \<longrightarrow> fun_apply(##Lset(i),rp,co,rpco) \<longrightarrow> 
             number1(##Lset(i),rpco),
                        bo) \<and> pair(##Lset(i),u,bo,x))]"
-apply (unfold is_bool_of_o_def) 
+  unfolding is_bool_of_o_def 
 apply (intro FOL_reflections function_reflections Cons_reflection)
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Constructible/Wellorderings.thy
--- a/src/ZF/Constructible/Wellorderings.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Constructible/Wellorderings.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -214,7 +214,7 @@
 
 lemma wellordered_subset: 
     "\<lbrakk>wellordered(M, A, r); B \<subseteq> A\<rbrakk> \<Longrightarrow> wellordered(M, B, r)"
-apply (unfold wellordered_def)
+  unfolding wellordered_def
 apply (blast intro: linear_rel_subset transitive_rel_subset 
                     wellfounded_on_subset)
 done
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Epsilon.thy
--- a/src/ZF/Epsilon.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Epsilon.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -40,7 +40,7 @@
 subsection\<open>Basic Closure Properties\<close>
 
 lemma arg_subset_eclose: "A \<subseteq> eclose(A)"
-apply (unfold eclose_def)
+  unfolding eclose_def
 apply (rule nat_rec_0 [THEN equalityD2, THEN subset_trans])
 apply (rule nat_0I [THEN UN_upper])
 done
@@ -86,7 +86,7 @@
 
 lemma eclose_least_lemma:
     "\<lbrakk>Transset(X);  A<=X;  n \<in> nat\<rbrakk> \<Longrightarrow> nat_rec(n, A, \<lambda>m r. \<Union>(r)) \<subseteq> X"
-apply (unfold Transset_def)
+  unfolding Transset_def
 apply (erule nat_induct)
 apply (simp add: nat_rec_0)
 apply (simp add: nat_rec_succ, blast)
@@ -94,7 +94,7 @@
 
 lemma eclose_least:
      "\<lbrakk>Transset(X);  A<=X\<rbrakk> \<Longrightarrow> eclose(A) \<subseteq> X"
-apply (unfold eclose_def)
+  unfolding eclose_def
 apply (rule eclose_least_lemma [THEN UN_least], assumption+)
 done
 
@@ -106,7 +106,7 @@
 \<rbrakk> \<Longrightarrow> P(a)"
 apply (rule eclose_least [THEN subsetD, THEN CollectD2, of "eclose(b)"])
   prefer 3 apply assumption
- apply (unfold Transset_def)
+   unfolding Transset_def
  apply (blast intro: ecloseD)
 apply (blast intro: arg_subset_eclose [THEN subsetD])
 done
@@ -168,7 +168,7 @@
 done
 
 lemma transrec: "transrec(a,H) = H(a, \<lambda>x\<in>a. transrec(x,H))"
-apply (unfold transrec_def)
+  unfolding transrec_def
 apply (rule wfrec_ssubst)
 apply (simp add: wfrec_eclose_eq2 arg_in_eclose_sing under_Memrel_eclose)
 done
@@ -291,13 +291,13 @@
 done
 
 lemma rank_pair1: "rank(a) < rank(\<langle>a,b\<rangle>)"
-apply (unfold Pair_def)
+  unfolding Pair_def
 apply (rule consI1 [THEN rank_lt, THEN lt_trans])
 apply (rule consI1 [THEN consI2, THEN rank_lt])
 done
 
 lemma rank_pair2: "rank(b) < rank(\<langle>a,b\<rangle>)"
-apply (unfold Pair_def)
+  unfolding Pair_def
 apply (rule consI1 [THEN consI2, THEN rank_lt, THEN lt_trans])
 apply (rule consI1 [THEN consI2, THEN rank_lt])
 done
@@ -380,12 +380,12 @@
 (** rec: old version for compatibility **)
 
 lemma rec_0 [simp]: "rec(0,a,b) = a"
-apply (unfold rec_def)
+  unfolding rec_def
 apply (rule recursor_0)
 done
 
 lemma rec_succ [simp]: "rec(succ(m),a,b) = b(m, rec(m,a,b))"
-apply (unfold rec_def)
+  unfolding rec_def
 apply (rule recursor_succ)
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/EquivClass.thy
--- a/src/ZF/EquivClass.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/EquivClass.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -45,7 +45,7 @@
 
 lemma equiv_comp_eq:
     "equiv(A,r) \<Longrightarrow> converse(r) O r = r"
-apply (unfold equiv_def)
+  unfolding equiv_def
 apply (blast del: subsetI intro!: sym_trans_comp_subset refl_comp_subset)
 done
 
@@ -66,7 +66,7 @@
 
 lemma equiv_class_eq:
     "\<lbrakk>equiv(A,r);  \<langle>a,b\<rangle>: r\<rbrakk> \<Longrightarrow> r``{a} = r``{b}"
-apply (unfold equiv_def)
+  unfolding equiv_def
 apply (safe del: subsetI intro!: equalityI equiv_class_subset)
 apply (unfold sym_def, blast)
 done
@@ -104,7 +104,7 @@
 (** Introduction/elimination rules -- needed? **)
 
 lemma quotientI [TC]: "x \<in> A \<Longrightarrow> r``{x}: A//r"
-apply (unfold quotient_def)
+  unfolding quotient_def
 apply (erule RepFunI)
 done
 
@@ -118,7 +118,7 @@
 
 lemma quotient_disj:
     "\<lbrakk>equiv(A,r);  X \<in> A//r;  Y \<in> A//r\<rbrakk> \<Longrightarrow> X=Y | (X \<inter> Y \<subseteq> 0)"
-apply (unfold quotient_def)
+  unfolding quotient_def
 apply (safe intro!: equiv_class_eq, assumption)
 apply (unfold equiv_def trans_def sym_def, blast)
 done
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Fixedpt.thy
--- a/src/ZF/Fixedpt.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Fixedpt.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -32,7 +32,7 @@
 by (unfold bnd_mono_def, clarify, blast)  
 
 lemma bnd_monoD1: "bnd_mono(D,h) \<Longrightarrow> h(D) \<subseteq> D"
-apply (unfold bnd_mono_def)
+  unfolding bnd_mono_def
 apply (erule conjunct1)
 done
 
@@ -45,7 +45,7 @@
 
 lemma bnd_mono_Un:
      "\<lbrakk>bnd_mono(D,h);  A \<subseteq> D;  B \<subseteq> D\<rbrakk> \<Longrightarrow> h(A) \<union> h(B) \<subseteq> h(A \<union> B)"
-apply (unfold bnd_mono_def)
+  unfolding bnd_mono_def
 apply (rule Un_least, blast+)
 done
 
@@ -53,7 +53,7 @@
 lemma bnd_mono_UN:
      "\<lbrakk>bnd_mono(D,h);  \<forall>i\<in>I. A(i) \<subseteq> D\<rbrakk> 
       \<Longrightarrow> (\<Union>i\<in>I. h(A(i))) \<subseteq> h((\<Union>i\<in>I. A(i)))"
-apply (unfold bnd_mono_def) 
+  unfolding bnd_mono_def 
 apply (rule UN_least)
 apply (elim conjE) 
 apply (drule_tac x="A(i)" in spec)
@@ -193,7 +193,7 @@
 
 (*gfp contains each post-fixedpoint that is contained in D*)
 lemma gfp_upperbound: "\<lbrakk>A \<subseteq> h(A);  A<=D\<rbrakk> \<Longrightarrow> A \<subseteq> gfp(D,h)"
-apply (unfold gfp_def)
+  unfolding gfp_def
 apply (rule PowI [THEN CollectI, THEN Union_upper])
 apply (assumption+)
 done
@@ -210,7 +210,7 @@
 lemma gfp_least: 
     "\<lbrakk>bnd_mono(D,h);  \<And>X. \<lbrakk>X \<subseteq> h(X);  X<=D\<rbrakk> \<Longrightarrow> X<=A\<rbrakk> \<Longrightarrow>  
      gfp(D,h) \<subseteq> A"
-apply (unfold gfp_def)
+  unfolding gfp_def
 apply (blast dest: bnd_monoD1) 
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/IMP/Equiv.thy
--- a/src/ZF/IMP/Equiv.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/IMP/Equiv.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -66,7 +66,7 @@
    apply safe
    apply simp_all
    apply (frule Gamma_bnd_mono [OF C_subset], erule Fixedpt.induct, assumption)
-   apply (unfold Gamma_def)
+     unfolding Gamma_def
    apply force
   txt \<open>\<open>if\<close>\<close>
   apply auto
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Induct/Comb.thy
--- a/src/ZF/Induct/Comb.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Induct/Comb.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -86,7 +86,7 @@
 lemma diamond_strip_lemmaD [rule_format]:
   "\<lbrakk>diamond(r);  \<langle>x,y\<rangle>:r^+\<rbrakk> \<Longrightarrow>
     \<forall>y'. <x,y'>:r \<longrightarrow> (\<exists>z. <y',z>: r^+ \<and> \<langle>y,z\<rangle>: r)"
-  apply (unfold diamond_def)
+    unfolding diamond_def
   apply (erule trancl_induct)
    apply (blast intro: r_into_trancl)
   apply clarify
@@ -186,7 +186,7 @@
   by (blast intro: comb_I)
 
 lemma not_diamond_contract: "\<not> diamond(contract)"
-  apply (unfold diamond_def)
+    unfolding diamond_def
   apply (blast intro: KIII_contract1 KIII_contract2 KIII_contract3
     elim!: I_contract_E)
   done
@@ -228,7 +228,7 @@
 
 lemma diamond_parcontract: "diamond(parcontract)"
   \<comment> \<open>Church-Rosser property for parallel contraction\<close>
-  apply (unfold diamond_def)
+    unfolding diamond_def
   apply (rule impI [THEN allI, THEN allI])
   apply (erule parcontract.induct)
      apply (blast elim!: comb.free_elims  intro: parcontract_combD2)+
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Induct/FoldSet.thy
--- a/src/ZF/Induct/FoldSet.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Induct/FoldSet.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -144,7 +144,7 @@
 
 lemma (in fold_typing) fold_equality: 
      "\<langle>C,y\<rangle> \<in> fold_set(A,B,f,e) \<Longrightarrow> fold[B](f,e,C) = y"
-apply (unfold fold_def)
+  unfolding fold_def
 apply (frule fold_set.dom_subset [THEN subsetD], clarify)
 apply (rule the_equality)
  apply (rule_tac [2] A=C in fold_typing.fold_set_determ)
@@ -155,7 +155,7 @@
 done
 
 lemma fold_0 [simp]: "e \<in> B \<Longrightarrow> fold[B](f,e,0) = e"
-apply (unfold fold_def)
+  unfolding fold_def
 apply (blast elim!: empty_fold_setE intro: fold_set.intros)
 done
 
@@ -193,7 +193,7 @@
 lemma (in fold_typing) fold_cons: 
      "\<lbrakk>C\<in>Fin(A); c\<in>A; c\<notin>C\<rbrakk> 
       \<Longrightarrow> fold[B](f, e, cons(c, C)) = f(c, fold[B](f, e, C))"
-apply (unfold fold_def)
+  unfolding fold_def
 apply (simp add: fold_cons_lemma)
 apply (rule the_equality, auto) 
  apply (subgoal_tac [2] "\<langle>C, y\<rangle> \<in> fold_set(A, B, f, e)")
@@ -363,7 +363,7 @@
      "\<lbrakk>setsum(f, A) = $# succ(n); n\<in>nat\<rbrakk>\<Longrightarrow> \<exists>a\<in>A. #0 $< f(a)"
 apply (case_tac "Finite (A) ")
 apply (blast intro: setsum_succD_lemma)
-apply (unfold setsum_def)
+  unfolding setsum_def
 apply (auto simp del: int_of_0 int_of_succ simp add: int_succ_int_1 [symmetric] int_of_0 [symmetric])
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Induct/Multiset.thy
--- a/src/ZF/Induct/Multiset.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Induct/Multiset.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -393,7 +393,7 @@
 done
 
 lemma msize_eq_succ_imp_elem: "\<lbrakk>msize(M)= $# succ(n); n \<in> nat\<rbrakk> \<Longrightarrow> \<exists>a. a \<in> mset_of(M)"
-apply (unfold msize_def)
+  unfolding msize_def
 apply (blast dest: setsum_succD)
 done
 
@@ -480,7 +480,7 @@
   (\<forall>a \<in> mset_of(M). setsum(\<lambda>z. $# mcount(M(a:=M`a #- 1), z), A) =
   (if a \<in> A then setsum(\<lambda>z. $# mcount(M, z), A) $- #1
            else setsum(\<lambda>z. $# mcount(M, z), A))))"
-apply (unfold multiset_def)
+  unfolding multiset_def
 apply (erule Finite_induct)
 apply (auto simp add: multiset_fun_iff)
 apply (unfold mset_of_def mcount_def)
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Induct/Primrec.thy
--- a/src/ZF/Induct/Primrec.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Induct/Primrec.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -240,7 +240,7 @@
 declare list_add_type [simp]
 
 lemma SC_case: "l \<in> list(nat) \<Longrightarrow> SC ` l < ack(1, list_add(l))"
-  apply (unfold SC_def)
+    unfolding SC_def
   apply (erule list.cases)
    apply (simp add: succ_iff)
   apply (simp add: ack_1 add_le_self)
@@ -260,7 +260,7 @@
 
 lemma PROJ_case [rule_format]:
     "l \<in> list(nat) \<Longrightarrow> \<forall>i \<in> nat. PROJ(i) ` l < ack(0, list_add(l))"
-  apply (unfold PROJ_def)
+    unfolding PROJ_def
   apply simp
   apply (erule list.induct)
    apply (simp add: nat_0_le)
@@ -322,7 +322,7 @@
      g \<in> prim_rec;  kg\<in>nat;
      l \<in> list(nat)\<rbrakk>
   \<Longrightarrow> PREC(f,g)`l #+ list_add(l) < ack(succ(kf#+kg), list_add(l))"
-  apply (unfold PREC_def)
+    unfolding PREC_def
   apply (erule list.cases)
    apply (simp add: lt_trans [OF nat_le_refl lt_ack2])
   apply simp
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Induct/PropLog.thy
--- a/src/ZF/Induct/PropLog.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Induct/PropLog.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -180,7 +180,7 @@
 subsubsection \<open>Soundness of the rules wrt truth-table semantics\<close>
 
 theorem soundness: "H |- p \<Longrightarrow> H |= p"
-  apply (unfold logcon_def)
+    unfolding logcon_def
   apply (induct set: thms)
       apply auto
   done
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Induct/Rmap.thy
--- a/src/ZF/Induct/Rmap.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Induct/Rmap.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -46,7 +46,7 @@
   done
 
 lemma rmap_functional: "function(r) \<Longrightarrow> function(rmap(r))"
-  apply (unfold function_def)
+    unfolding function_def
   apply (rule impI [THEN allI, THEN allI])
   apply (erule rmap.induct)
    apply blast+
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Induct/Term.thy
--- a/src/ZF/Induct/Term.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Induct/Term.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -169,7 +169,7 @@
 
 lemma term_map_type [TC]:
     "\<lbrakk>t \<in> term(A);  \<And>x. x \<in> A \<Longrightarrow> f(x): B\<rbrakk> \<Longrightarrow> term_map(f,t) \<in> term(B)"
-  apply (unfold term_map_def)
+    unfolding term_map_def
   apply (erule term_rec_simple_type)
   apply fast
   done
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Induct/Tree_Forest.thy
--- a/src/ZF/Induct/Tree_Forest.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Induct/Tree_Forest.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -109,7 +109,7 @@
 \<rbrakk> \<Longrightarrow> (\<forall>t \<in> tree(A).    tree_forest_rec(b,c,d,t) \<in> C(t)) \<and>
           (\<forall>f \<in> forest(A). tree_forest_rec(b,c,d,f) \<in> D(f))"
     \<comment> \<open>Mutually recursive version.\<close>
-  apply (unfold Ball_def)
+    unfolding Ball_def
   apply (rule tree_forest.mutual_induct)
   apply simp_all
   done
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/IntDiv.thy
--- a/src/ZF/IntDiv.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/IntDiv.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -688,12 +688,12 @@
 done
 
 lemma negateSnd_eq [simp]: "negateSnd (\<langle>q,r\<rangle>) = <q, $-r>"
-apply (unfold negateSnd_def)
+  unfolding negateSnd_def
 apply auto
 done
 
 lemma negateSnd_type: "qr \<in> int * int \<Longrightarrow> negateSnd (qr) \<in> int * int"
-apply (unfold negateSnd_def)
+  unfolding negateSnd_def
 apply auto
 done
 
@@ -735,7 +735,7 @@
   by (simp add: zdiv_def)
 
 lemma zdiv_type [iff,TC]: "z zdiv w \<in> int"
-apply (unfold zdiv_def)
+  unfolding zdiv_def
 apply (blast intro: fst_type divAlg_type)
 done
 
@@ -746,7 +746,7 @@
   by (simp add: zmod_def)
 
 lemma zmod_type [iff,TC]: "z zmod w \<in> int"
-apply (unfold zmod_def)
+  unfolding zmod_def
 apply (rule snd_type)
 apply (blast intro: divAlg_type)
 done
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/List.thy
--- a/src/ZF/List.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/List.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -267,7 +267,7 @@
 (** set_of_list **)
 
 lemma set_of_list_type [TC]: "l \<in> list(A) \<Longrightarrow> set_of_list(l) \<in> Pow(A)"
-apply (unfold set_of_list_list_def)
+  unfolding set_of_list_list_def
 apply (erule list_rec_type, auto)
 done
 
@@ -463,7 +463,7 @@
 (** min FIXME: replace by Int! **)
 (* Min theorems are also true for i, j ordinals *)
 lemma min_sym: "\<lbrakk>i \<in> nat; j \<in> nat\<rbrakk> \<Longrightarrow> min(i,j)=min(j,i)"
-apply (unfold min_def)
+  unfolding min_def
 apply (auto dest!: not_lt_imp_le dest: lt_not_sym intro: le_anti_sym)
 done
 
@@ -471,17 +471,17 @@
 by (unfold min_def, auto)
 
 lemma min_0 [simp]: "i \<in> nat \<Longrightarrow> min(0,i) = 0"
-apply (unfold min_def)
+  unfolding min_def
 apply (auto dest: not_lt_imp_le)
 done
 
 lemma min_02 [simp]: "i \<in> nat \<Longrightarrow> min(i, 0) = 0"
-apply (unfold min_def)
+  unfolding min_def
 apply (auto dest: not_lt_imp_le)
 done
 
 lemma lt_min_iff: "\<lbrakk>i \<in> nat; j \<in> nat; k \<in> nat\<rbrakk> \<Longrightarrow> i<min(j,k) \<longleftrightarrow> i<j \<and> i<k"
-apply (unfold min_def)
+  unfolding min_def
 apply (auto dest!: not_lt_imp_le intro: lt_trans2 lt_trans)
 done
 
@@ -689,7 +689,7 @@
 (** take **)
 
 lemma take_0 [simp]: "xs:list(A) \<Longrightarrow> take(0, xs) =  Nil"
-apply (unfold take_def)
+  unfolding take_def
 apply (erule list.induct, auto)
 done
 
@@ -917,7 +917,7 @@
 lemma length_zip [rule_format]:
      "xs:list(A) \<Longrightarrow> \<forall>ys \<in> list(B). length(zip(xs,ys)) =
                                      min(length(xs), length(ys))"
-apply (unfold min_def)
+  unfolding min_def
 apply (induct_tac "xs", simp_all, clarify)
 apply (erule_tac a = ys in list.cases, auto)
 done
@@ -1200,7 +1200,7 @@
 
 lemma sublist_type [simp,TC]:
      "xs:list(B) \<Longrightarrow> sublist(xs, A):list(B)"
-apply (unfold sublist_def)
+  unfolding sublist_def
 apply (induct_tac "xs")
 apply (auto simp add: filter_append map_app_distrib)
 done
@@ -1212,7 +1212,7 @@
 lemma sublist_append:
  "\<lbrakk>xs:list(B); ys:list(B)\<rbrakk> \<Longrightarrow>
   sublist(xs@ys, A) = sublist(xs, A) @ sublist(ys, {j \<in> nat. j #+ length(xs): A})"
-apply (unfold sublist_def)
+  unfolding sublist_def
 apply (erule_tac l = ys in list_append_induct, simp)
 apply (simp (no_asm_simp) add: upt_add_eq_append2 app_assoc [symmetric])
 apply (auto simp add: sublist_shift_lemma length_type map_app_distrib app_assoc)
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Nat.thy
--- a/src/ZF/Nat.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Nat.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -108,13 +108,13 @@
 lemma Ord_nat [iff]: "Ord(nat)"
 apply (rule OrdI)
 apply (erule_tac [2] nat_into_Ord [THEN Ord_is_Transset])
-apply (unfold Transset_def)
+  unfolding Transset_def
 apply (rule ballI)
 apply (erule nat_induct, auto)
 done
 
 lemma Limit_nat [iff]: "Limit(nat)"
-apply (unfold Limit_def)
+  unfolding Limit_def
 apply (safe intro!: ltI Ord_nat)
 apply (erule ltD)
 done
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Order.thy
--- a/src/ZF/Order.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Order.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -142,13 +142,13 @@
 
 lemma tot_ord_subset:
     "\<lbrakk>tot_ord(A,r);  B<=A\<rbrakk> \<Longrightarrow> tot_ord(B,r)"
-apply (unfold tot_ord_def)
+  unfolding tot_ord_def
 apply (fast elim!: part_ord_subset linear_subset)
 done
 
 lemma well_ord_subset:
     "\<lbrakk>well_ord(A,r);  B<=A\<rbrakk> \<Longrightarrow> well_ord(B,r)"
-apply (unfold well_ord_def)
+  unfolding well_ord_def
 apply (fast elim!: tot_ord_subset wf_on_subset_A)
 done
 
@@ -162,7 +162,7 @@
 by (unfold trans_on_def, blast)
 
 lemma part_ord_Int_iff: "part_ord(A,r \<inter> A*A) \<longleftrightarrow> part_ord(A,r)"
-apply (unfold part_ord_def)
+  unfolding part_ord_def
 apply (simp add: irrefl_Int_iff trans_on_Int_iff)
 done
 
@@ -170,7 +170,7 @@
 by (unfold linear_def, blast)
 
 lemma tot_ord_Int_iff: "tot_ord(A,r \<inter> A*A) \<longleftrightarrow> tot_ord(A,r)"
-apply (unfold tot_ord_def)
+  unfolding tot_ord_def
 apply (simp add: part_ord_Int_iff linear_Int_iff)
 done
 
@@ -179,7 +179,7 @@
 done
 
 lemma well_ord_Int_iff: "well_ord(A,r \<inter> A*A) \<longleftrightarrow> well_ord(A,r)"
-apply (unfold well_ord_def)
+  unfolding well_ord_def
 apply (simp add: tot_ord_Int_iff wf_on_Int_iff)
 done
 
@@ -199,7 +199,7 @@
 by (unfold trans_on_def, blast)
 
 lemma part_ord_0: "part_ord(0,r)"
-apply (unfold part_ord_def)
+  unfolding part_ord_def
 apply (simp add: irrefl_0 trans_on_0)
 done
 
@@ -207,7 +207,7 @@
 by (unfold linear_def, blast)
 
 lemma tot_ord_0: "tot_ord(0,r)"
-apply (unfold tot_ord_def)
+  unfolding tot_ord_def
 apply (simp add: part_ord_0 linear_0)
 done
 
@@ -215,7 +215,7 @@
 by (unfold wf_on_def wf_def, blast)
 
 lemma well_ord_0: "well_ord(0,r)"
-apply (unfold well_ord_def)
+  unfolding well_ord_def
 apply (simp add: tot_ord_0 wf_on_0)
 done
 
@@ -228,7 +228,7 @@
 by (simp add: irrefl_def trans_on_def part_ord_def linear_def tot_ord_def)
 
 lemma well_ord_unit: "well_ord({a},0)"
-apply (unfold well_ord_def)
+  unfolding well_ord_def
 apply (simp add: tot_ord_unit wf_on_any_0)
 done
 
@@ -297,7 +297,7 @@
 lemma mono_map_trans:
     "\<lbrakk>g \<in> mono_map(A,r,B,s);  f \<in> mono_map(B,s,C,t)\<rbrakk>
      \<Longrightarrow> (f O g): mono_map(A,r,C,t)"
-apply (unfold mono_map_def)
+  unfolding mono_map_def
 apply (auto simp add: comp_fun)
 done
 
@@ -494,7 +494,7 @@
 
 lemma converse_ord_iso_map:
     "converse(ord_iso_map(A,r,B,s)) = ord_iso_map(B,s,A,r)"
-apply (unfold ord_iso_map_def)
+  unfolding ord_iso_map_def
 apply (blast intro: ord_iso_sym)
 done
 
@@ -514,12 +514,12 @@
      \<Longrightarrow> ord_iso_map(A,r,B,s)
            \<in> mono_map(domain(ord_iso_map(A,r,B,s)), r,
                       range(ord_iso_map(A,r,B,s)), s)"
-apply (unfold mono_map_def)
+  unfolding mono_map_def
 apply (simp (no_asm_simp) add: ord_iso_map_fun)
 apply safe
 apply (subgoal_tac "x \<in> A \<and> ya:A \<and> y \<in> B \<and> yb:B")
  apply (simp add: apply_equality [OF _  ord_iso_map_fun])
- apply (unfold ord_iso_map_def)
+   unfolding ord_iso_map_def
  apply (blast intro: well_ord_iso_preserving, blast)
 done
 
@@ -542,7 +542,7 @@
      "\<lbrakk>well_ord(A,r);  well_ord(B,s);
          a \<in> A;  a \<notin> domain(ord_iso_map(A,r,B,s))\<rbrakk>
       \<Longrightarrow>  domain(ord_iso_map(A,r,B,s)) \<subseteq> pred(A, a, r)"
-apply (unfold ord_iso_map_def)
+  unfolding ord_iso_map_def
 apply (safe intro!: predI)
 (*Case analysis on  xa vs a in r *)
 apply (simp (no_asm_simp))
@@ -621,7 +621,7 @@
 by (unfold trans_on_def, blast)
 
 lemma part_ord_converse: "part_ord(A,r) \<Longrightarrow> part_ord(A,converse(r))"
-apply (unfold part_ord_def)
+  unfolding part_ord_def
 apply (blast intro!: irrefl_converse trans_on_converse)
 done
 
@@ -629,7 +629,7 @@
 by (unfold linear_def, blast)
 
 lemma tot_ord_converse: "tot_ord(A,r) \<Longrightarrow> tot_ord(A,converse(r))"
-apply (unfold tot_ord_def)
+  unfolding tot_ord_def
 apply (blast intro!: part_ord_converse linear_converse)
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/OrderArith.thy
--- a/src/ZF/OrderArith.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/OrderArith.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -69,7 +69,7 @@
 subsubsection\<open>Type checking\<close>
 
 lemma radd_type: "radd(A,r,B,s) \<subseteq> (A+B) * (A+B)"
-apply (unfold radd_def)
+  unfolding radd_def
 apply (rule Collect_subset)
 done
 
@@ -127,7 +127,7 @@
     "\<lbrakk>f \<in> ord_iso(A,r,A',r');  g \<in> ord_iso(B,s,B',s')\<rbrakk> \<Longrightarrow>
             (\<lambda>z\<in>A+B. case(\<lambda>x. Inl(f`x), \<lambda>y. Inr(g`y), z))
             \<in> ord_iso(A+B, radd(A,r,B,s), A'+B', radd(A',r',B',s'))"
-apply (unfold ord_iso_def)
+  unfolding ord_iso_def
 apply (safe intro!: sum_bij)
 (*Do the beta-reductions now*)
 apply (auto cong add: conj_cong simp add: bij_is_fun [THEN apply_type])
@@ -232,7 +232,7 @@
     "\<lbrakk>f \<in> ord_iso(A,r,A',r');  g \<in> ord_iso(B,s,B',s')\<rbrakk>
      \<Longrightarrow> (lam \<langle>x,y\<rangle>:A*B. \<langle>f`x, g`y\<rangle>)
          \<in> ord_iso(A*B, rmult(A,r,B,s), A'*B', rmult(A',r',B',s'))"
-apply (unfold ord_iso_def)
+  unfolding ord_iso_def
 apply (safe intro!: prod_bij)
 apply (simp_all add: bij_is_fun [THEN apply_type])
 apply (blast intro: bij_is_inj [THEN inj_apply_equality])
@@ -337,7 +337,7 @@
 
 lemma part_ord_rvimage:
     "\<lbrakk>f \<in> inj(A,B);  part_ord(B,r)\<rbrakk> \<Longrightarrow> part_ord(A, rvimage(A,f,r))"
-apply (unfold part_ord_def)
+  unfolding part_ord_def
 apply (blast intro!: irrefl_rvimage trans_on_rvimage)
 done
 
@@ -351,7 +351,7 @@
 
 lemma tot_ord_rvimage:
     "\<lbrakk>f \<in> inj(A,B);  tot_ord(B,r)\<rbrakk> \<Longrightarrow> tot_ord(A, rvimage(A,f,r))"
-apply (unfold tot_ord_def)
+  unfolding tot_ord_def
 apply (blast intro!: part_ord_rvimage linear_rvimage)
 done
 
@@ -391,7 +391,7 @@
 
 lemma ord_iso_rvimage:
     "f \<in> bij(A,B) \<Longrightarrow> f \<in> ord_iso(A, rvimage(A,f,s), B, s)"
-apply (unfold ord_iso_def)
+  unfolding ord_iso_def
 apply (simp add: rvimage_iff)
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/OrderType.thy
--- a/src/ZF/OrderType.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/OrderType.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -80,7 +80,7 @@
 apply (frule lt_pred_Memrel)
 apply (erule ltE)
 apply (rule well_ord_Memrel [THEN well_ord_iso_predE, of i f j], auto)
-apply (unfold ord_iso_def)
+  unfolding ord_iso_def
 (*Combining the two simplifications causes looping*)
 apply (simp (no_asm_simp))
 apply (blast intro: bij_is_fun [THEN apply_type] Ord_trans)
@@ -156,7 +156,7 @@
 
 lemma Ord_ordertype:
     "well_ord(A,r) \<Longrightarrow> Ord(ordertype(A,r))"
-apply (unfold ordertype_def)
+  unfolding ordertype_def
 apply (subst image_fun [OF ordermap_type subset_refl])
 apply (rule OrdI [OF _ Ord_is_Transset])
 prefer 2 apply (blast intro: Ord_ordermap)
@@ -201,7 +201,7 @@
 lemma ordertype_ord_iso:
  "well_ord(A,r)
   \<Longrightarrow> ordermap(A,r) \<in> ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))"
-apply (unfold ord_iso_def)
+  unfolding ord_iso_def
 apply (safe elim!: well_ord_is_wf
             intro!: ordermap_type [THEN apply_type] ordermap_mono ordermap_bij)
 apply (blast dest!: converse_ordermap_mono)
@@ -272,7 +272,7 @@
 
 lemma ordertype_unfold:
     "ordertype(A,r) = {ordermap(A,r)`y . y \<in> A}"
-apply (unfold ordertype_def)
+  unfolding ordertype_def
 apply (rule image_fun [OF ordermap_type subset_refl])
 done
 
@@ -311,7 +311,7 @@
 
 (*proof by Krzysztof Grabczewski*)
 lemma Ord_is_Ord_alt: "Ord(i) \<Longrightarrow> Ord_alt(i)"
-apply (unfold Ord_alt_def)
+  unfolding Ord_alt_def
 apply (rule conjI)
 apply (erule well_ord_Memrel)
 apply (unfold Ord_def Transset_def pred_def Memrel_def, blast)
@@ -363,7 +363,7 @@
 lemma pred_Inl_bij:
  "a \<in> A \<Longrightarrow> (\<lambda>x\<in>pred(A,a,r). Inl(x))
           \<in> bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))"
-apply (unfold pred_def)
+  unfolding pred_def
 apply (rule_tac d = "case (\<lambda>x. x, \<lambda>y. y) " in lam_bijective)
 apply auto
 done
@@ -709,7 +709,7 @@
 
 lemma Ord_odiff [simp,TC]:
     "\<lbrakk>Ord(i);  Ord(j)\<rbrakk> \<Longrightarrow> Ord(i--j)"
-apply (unfold odiff_def)
+  unfolding odiff_def
 apply (blast intro: Ord_ordertype Diff_subset well_ord_subset well_ord_Memrel)
 done
 
@@ -750,7 +750,7 @@
 
 lemma Ord_omult [simp,TC]:
     "\<lbrakk>Ord(i);  Ord(j)\<rbrakk> \<Longrightarrow> Ord(i**j)"
-apply (unfold omult_def)
+  unfolding omult_def
 apply (blast intro: Ord_ordertype well_ord_rmult well_ord_Memrel)
 done
 
@@ -797,7 +797,7 @@
 lemma lt_omult:
  "\<lbrakk>Ord(i);  Ord(j);  k<j**i\<rbrakk>
   \<Longrightarrow> \<exists>j' i'. k = j**i' ++ j' \<and> j'<j \<and> i'<i"
-apply (unfold omult_def)
+  unfolding omult_def
 apply (simp add: ordertype_pred_unfold well_ord_rmult well_ord_Memrel)
 apply (safe elim!: ltE)
 apply (simp add: ordertype_pred_Pair_lemma ltI raw_oadd_eq_oadd
@@ -807,7 +807,7 @@
 
 lemma omult_oadd_lt:
      "\<lbrakk>j'<j;  i'<i\<rbrakk> \<Longrightarrow> j**i' ++ j'  <  j**i"
-apply (unfold omult_def)
+  unfolding omult_def
 apply (rule ltI)
  prefer 2
  apply (simp add: Ord_ordertype well_ord_rmult well_ord_Memrel lt_Ord2)
@@ -834,19 +834,19 @@
 text\<open>Ordinal multiplication by zero\<close>
 
 lemma omult_0 [simp]: "i**0 = 0"
-apply (unfold omult_def)
+  unfolding omult_def
 apply (simp (no_asm_simp))
 done
 
 lemma omult_0_left [simp]: "0**i = 0"
-apply (unfold omult_def)
+  unfolding omult_def
 apply (simp (no_asm_simp))
 done
 
 text\<open>Ordinal multiplication by 1\<close>
 
 lemma omult_1 [simp]: "Ord(i) \<Longrightarrow> i**1 = i"
-apply (unfold omult_def)
+  unfolding omult_def
 apply (rule_tac s1="Memrel(i)"
        in ord_isoI [THEN ordertype_eq, THEN trans])
 apply (rule_tac c = snd and d = "\<lambda>z.\<langle>0,z\<rangle>"  in lam_bijective)
@@ -854,7 +854,7 @@
 done
 
 lemma omult_1_left [simp]: "Ord(i) \<Longrightarrow> 1**i = i"
-apply (unfold omult_def)
+  unfolding omult_def
 apply (rule_tac s1="Memrel(i)"
        in ord_isoI [THEN ordertype_eq, THEN trans])
 apply (rule_tac c = fst and d = "\<lambda>z.\<langle>z,0\<rangle>" in lam_bijective)
@@ -886,7 +886,7 @@
 
 lemma omult_assoc:
     "\<lbrakk>Ord(i);  Ord(j);  Ord(k)\<rbrakk> \<Longrightarrow> (i**j)**k = i**(j**k)"
-apply (unfold omult_def)
+  unfolding omult_def
 apply (rule ordertype_eq [THEN trans])
 apply (rule prod_ord_iso_cong [OF ord_iso_refl
                                   ordertype_ord_iso [THEN ord_iso_sym]])
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Ordinal.thy
--- a/src/ZF/Ordinal.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Ordinal.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -40,7 +40,7 @@
 by (unfold Transset_def, blast)
 
 lemma Transset_iff_Union_succ: "Transset(A) <-> \<Union>(succ(A)) = A"
-apply (unfold Transset_def)
+  unfolding Transset_def
 apply (blast elim!: equalityE)
 done
 
@@ -157,12 +157,12 @@
 by (blast intro: Ord_succ dest!: Ord_succD)
 
 lemma Ord_Un [intro,simp,TC]: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> Ord(i \<union> j)"
-apply (unfold Ord_def)
+  unfolding Ord_def
 apply (blast intro!: Transset_Un)
 done
 
 lemma Ord_Int [TC]: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> Ord(i \<inter> j)"
-apply (unfold Ord_def)
+  unfolding Ord_def
 apply (blast intro!: Transset_Int)
 done
 
@@ -188,7 +188,7 @@
 
 lemma ltE:
     "\<lbrakk>i<j;  \<lbrakk>i\<in>j;  Ord(i);  Ord(j)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
-apply (unfold lt_def)
+  unfolding lt_def
 apply (blast intro: Ord_in_Ord)
 done
 
@@ -214,7 +214,7 @@
 by (blast intro!: ltI elim!: ltE intro: Ord_trans)
 
 lemma lt_not_sym: "i<j \<Longrightarrow> \<not> (j<i)"
-apply (unfold lt_def)
+  unfolding lt_def
 apply (blast elim: mem_asym)
 done
 
@@ -297,7 +297,7 @@
 (*The membership relation (as a set) is well-founded.
   Proof idea: show A<=B by applying the foundation axiom to A-B *)
 lemma wf_Memrel: "wf(Memrel(A))"
-apply (unfold wf_def)
+  unfolding wf_def
 apply (rule foundation [THEN disjE, THEN allI], erule disjI1, blast)
 done
 
@@ -630,17 +630,17 @@
 subsection\<open>Limit Ordinals -- General Properties\<close>
 
 lemma Limit_Union_eq: "Limit(i) \<Longrightarrow> \<Union>(i) = i"
-apply (unfold Limit_def)
+  unfolding Limit_def
 apply (fast intro!: ltI elim!: ltE elim: Ord_trans)
 done
 
 lemma Limit_is_Ord: "Limit(i) \<Longrightarrow> Ord(i)"
-apply (unfold Limit_def)
+  unfolding Limit_def
 apply (erule conjunct1)
 done
 
 lemma Limit_has_0: "Limit(i) \<Longrightarrow> 0 < i"
-apply (unfold Limit_def)
+  unfolding Limit_def
 apply (erule conjunct2 [THEN conjunct1])
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Perm.thy
--- a/src/ZF/Perm.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Perm.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -42,17 +42,17 @@
 subsection\<open>Surjective Function Space\<close>
 
 lemma surj_is_fun: "f \<in> surj(A,B) \<Longrightarrow> f \<in> A->B"
-apply (unfold surj_def)
+  unfolding surj_def
 apply (erule CollectD1)
 done
 
 lemma fun_is_surj: "f \<in> Pi(A,B) \<Longrightarrow> f \<in> surj(A,range(f))"
-apply (unfold surj_def)
+  unfolding surj_def
 apply (blast intro: apply_equality range_of_fun domain_type)
 done
 
 lemma surj_range: "f \<in> surj(A,B) \<Longrightarrow> range(f)=B"
-apply (unfold surj_def)
+  unfolding surj_def
 apply (best intro: apply_Pair elim: range_type)
 done
 
@@ -83,14 +83,14 @@
 subsection\<open>Injective Function Space\<close>
 
 lemma inj_is_fun: "f \<in> inj(A,B) \<Longrightarrow> f \<in> A->B"
-apply (unfold inj_def)
+  unfolding inj_def
 apply (erule CollectD1)
 done
 
 text\<open>Good for dealing with sets of pairs, but a bit ugly in use [used in AC]\<close>
 lemma inj_equality:
     "\<lbrakk>\<langle>a,b\<rangle>:f;  \<langle>c,b\<rangle>:f;  f \<in> inj(A,B)\<rbrakk> \<Longrightarrow> a=c"
-apply (unfold inj_def)
+  unfolding inj_def
 apply (blast dest: Pair_mem_PiD)
 done
 
@@ -115,12 +115,12 @@
 subsection\<open>Bijections\<close>
 
 lemma bij_is_inj: "f \<in> bij(A,B) \<Longrightarrow> f \<in> inj(A,B)"
-apply (unfold bij_def)
+  unfolding bij_def
 apply (erule IntD1)
 done
 
 lemma bij_is_surj: "f \<in> bij(A,B) \<Longrightarrow> f \<in> surj(A,B)"
-apply (unfold bij_def)
+  unfolding bij_def
 apply (erule IntD2)
 done
 
@@ -133,7 +133,7 @@
         \<And>x. x \<in> A \<Longrightarrow> d(c(x)) = x;
         \<And>y. y \<in> B \<Longrightarrow> c(d(y)) = y
 \<rbrakk> \<Longrightarrow> (\<lambda>x\<in>A. c(x)) \<in> bij(A,B)"
-apply (unfold bij_def)
+  unfolding bij_def
 apply (blast intro!: lam_injective lam_surjective)
 done
 
@@ -147,7 +147,7 @@
 subsection\<open>Identity Function\<close>
 
 lemma idI [intro!]: "a \<in> A \<Longrightarrow> \<langle>a,a\<rangle> \<in> id(A)"
-apply (unfold id_def)
+  unfolding id_def
 apply (erule lamI)
 done
 
@@ -155,17 +155,17 @@
 by (simp add: id_def lam_def, blast)
 
 lemma id_type: "id(A) \<in> A->A"
-apply (unfold id_def)
+  unfolding id_def
 apply (rule lam_type, assumption)
 done
 
 lemma id_conv [simp]: "x \<in> A \<Longrightarrow> id(A)`x = x"
-apply (unfold id_def)
+  unfolding id_def
 apply (simp (no_asm_simp))
 done
 
 lemma id_mono: "A<=B \<Longrightarrow> id(A) \<subseteq> id(B)"
-apply (unfold id_def)
+  unfolding id_def
 apply (erule lam_mono)
 done
 
@@ -182,12 +182,12 @@
 done
 
 lemma id_bij: "id(A): bij(A,A)"
-apply (unfold bij_def)
+  unfolding bij_def
 apply (blast intro: id_inj id_surj)
 done
 
 lemma subset_iff_id: "A \<subseteq> B \<longleftrightarrow> id(A) \<in> A->B"
-apply (unfold id_def)
+  unfolding id_def
 apply (force intro!: lam_type dest: apply_type)
 done
 
@@ -199,7 +199,7 @@
 subsection\<open>Converse of a Function\<close>
 
 lemma inj_converse_fun: "f \<in> inj(A,B) \<Longrightarrow> converse(f) \<in> range(f)->A"
-apply (unfold inj_def)
+  unfolding inj_def
 apply (simp (no_asm_simp) add: Pi_iff function_def)
 apply (erule CollectE)
 apply (simp (no_asm_simp) add: apply_iff)
@@ -251,7 +251,7 @@
 
 text\<open>Adding this as an intro! rule seems to cause looping\<close>
 lemma bij_converse_bij [TC]: "f \<in> bij(A,B) \<Longrightarrow> converse(f): bij(B,A)"
-apply (unfold bij_def)
+  unfolding bij_def
 apply (fast elim: surj_range [THEN subst] inj_converse_inj inj_converse_surj)
 done
 
@@ -372,13 +372,13 @@
 
 lemma comp_surj:
     "\<lbrakk>g \<in> surj(A,B);  f \<in> surj(B,C)\<rbrakk> \<Longrightarrow> (f O g) \<in> surj(A,C)"
-apply (unfold surj_def)
+  unfolding surj_def
 apply (blast intro!: comp_fun comp_fun_apply)
 done
 
 lemma comp_bij:
     "\<lbrakk>g \<in> bij(A,B);  f \<in> bij(B,C)\<rbrakk> \<Longrightarrow> (f O g) \<in> bij(A,C)"
-apply (unfold bij_def)
+  unfolding bij_def
 apply (blast intro: comp_inj comp_surj)
 done
 
@@ -405,7 +405,7 @@
 
 lemma comp_mem_surjD1:
     "\<lbrakk>(f O g): surj(A,C);  g \<in> A->B;  f \<in> B->C\<rbrakk> \<Longrightarrow> f \<in> surj(B,C)"
-apply (unfold surj_def)
+  unfolding surj_def
 apply (blast intro!: comp_fun_apply [symmetric] apply_funtype)
 done
 
@@ -452,7 +452,7 @@
 
 lemma fg_imp_bijective:
     "\<lbrakk>f \<in> A->B;  g \<in> B->A;  f O g = id(B);  g O f = id(A)\<rbrakk> \<Longrightarrow> f \<in> bij(A,B)"
-apply (unfold bij_def)
+  unfolding bij_def
 apply (simp add: comp_eq_id_iff)
 apply (blast intro: f_imp_injective f_imp_surjective apply_funtype)
 done
@@ -513,7 +513,7 @@
 
 lemma restrict_inj:
     "\<lbrakk>f \<in> inj(A,B);  C<=A\<rbrakk> \<Longrightarrow> restrict(f,C): inj(C,B)"
-apply (unfold inj_def)
+  unfolding inj_def
 apply (safe elim!: restrict_type2, auto)
 done
 
@@ -532,14 +532,14 @@
 subsubsection\<open>Lemmas for Ramsey's Theorem\<close>
 
 lemma inj_weaken_type: "\<lbrakk>f \<in> inj(A,B);  B<=D\<rbrakk> \<Longrightarrow> f \<in> inj(A,D)"
-apply (unfold inj_def)
+  unfolding inj_def
 apply (blast intro: fun_weaken_type)
 done
 
 lemma inj_succ_restrict:
      "\<lbrakk>f \<in> inj(succ(m), A)\<rbrakk> \<Longrightarrow> restrict(f,m) \<in> inj(m, A-{f`m})"
 apply (rule restrict_bij [THEN bij_is_inj, THEN inj_weaken_type], assumption, blast)
-apply (unfold inj_def)
+  unfolding inj_def
 apply (fast elim: range_type mem_irrefl dest: apply_equality)
 done
 
@@ -547,7 +547,7 @@
 lemma inj_extend:
     "\<lbrakk>f \<in> inj(A,B);  a\<notin>A;  b\<notin>B\<rbrakk>
      \<Longrightarrow> cons(\<langle>a,b\<rangle>,f) \<in> inj(cons(a,A), cons(b,B))"
-apply (unfold inj_def)
+  unfolding inj_def
 apply (force intro: apply_type  simp add: fun_extend)
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/QUniv.thy
--- a/src/ZF/QUniv.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/QUniv.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -47,7 +47,7 @@
 by (simp add: quniv_def)
 
 lemma quniv_mono: "A<=B \<Longrightarrow> quniv(A) \<subseteq> quniv(B)"
-apply (unfold quniv_def)
+  unfolding quniv_def
 apply (erule eclose_mono [THEN univ_mono, THEN Pow_mono])
 done
 
@@ -67,7 +67,7 @@
 lemmas univ_into_quniv = univ_subset_quniv [THEN subsetD]
 
 lemma Pow_univ_subset_quniv: "Pow(univ(A)) \<subseteq> quniv(A)"
-apply (unfold quniv_def)
+  unfolding quniv_def
 apply (rule arg_subset_eclose [THEN univ_mono, THEN Pow_mono])
 done
 
@@ -92,7 +92,7 @@
 subsection\<open>Quine Disjoint Sum\<close>
 
 lemma QInl_subset_univ: "a \<subseteq> univ(A) \<Longrightarrow> QInl(a) \<subseteq> univ(A)"
-apply (unfold QInl_def)
+  unfolding QInl_def
 apply (erule empty_subsetI [THEN QPair_subset_univ])
 done
 
@@ -103,7 +103,7 @@
     subset_trans [OF naturals_subset_nat nat_subset_univ]
 
 lemma QInr_subset_univ: "a \<subseteq> univ(A) \<Longrightarrow> QInr(a) \<subseteq> univ(A)"
-apply (unfold QInr_def)
+  unfolding QInr_def
 apply (erule nat_1I [THEN naturals_subset_univ, THEN QPair_subset_univ])
 done
 
@@ -178,7 +178,7 @@
 lemma QPair_Int_Vfrom_subset:
  "Transset(X) \<Longrightarrow>
        <a;b> \<inter> Vfrom(X,i)  \<subseteq>  <a \<inter> Vfrom(X,i);  b \<inter> Vfrom(X,i)>"
-apply (unfold QPair_def)
+  unfolding QPair_def
 apply (erule Transset_Vfrom [THEN Transset_sum_Int_subset])
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Resid/Confluence.thy
--- a/src/ZF/Resid/Confluence.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Resid/Confluence.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -110,7 +110,7 @@
 apply (blast intro: red1D1 redD2)
 apply (blast intro: red1D1 redD2)
 apply (cut_tac confluence_beta_reduction)
-apply (unfold confluence_def)
+  unfolding confluence_def
 apply (blast intro: Sred.trans)
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Resid/Residuals.thy
--- a/src/ZF/Resid/Residuals.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Resid/Residuals.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -85,21 +85,21 @@
 
 lemma res_Fun [simp]: 
     "\<lbrakk>s \<sim> t; regular(t)\<rbrakk>\<Longrightarrow> Fun(s) |> Fun(t) = Fun(s |> t)"
-apply (unfold res_func_def)
+  unfolding res_func_def
 apply (blast intro: comp_resfuncD residuals_function) 
 done
 
 lemma res_App [simp]: 
     "\<lbrakk>s \<sim> u; regular(u); t \<sim> v; regular(v); b \<in> bool\<rbrakk>
      \<Longrightarrow> App(b,s,t) |> App(0,u,v) = App(b, s |> u, t |> v)"
-apply (unfold res_func_def) 
+  unfolding res_func_def 
 apply (blast dest!: comp_resfuncD intro: residuals_function)
 done
 
 lemma res_redex [simp]: 
     "\<lbrakk>s \<sim> u; regular(u); t \<sim> v; regular(v); b \<in> bool\<rbrakk>
      \<Longrightarrow> App(b,Fun(s),t) |> App(1,Fun(u),v) = (t |> v)/ (s |> u)"
-apply (unfold res_func_def)
+  unfolding res_func_def
 apply (blast elim!: redexes.free_elims dest!: comp_resfuncD 
              intro: residuals_function)
 done
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Sum.thy
--- a/src/ZF/Sum.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Sum.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -29,7 +29,7 @@
 
 lemma Part_iff:
     "a \<in> Part(A,h) \<longleftrightarrow> a \<in> A \<and> (\<exists>y. a=h(y))"
-apply (unfold Part_def)
+  unfolding Part_def
 apply (rule separation)
 done
 
@@ -46,7 +46,7 @@
 done
 
 lemma Part_subset: "Part(A,h) \<subseteq> A"
-apply (unfold Part_def)
+  unfolding Part_def
 apply (rule Collect_subset)
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Trancl.thy
--- a/src/ZF/Trancl.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Trancl.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -101,7 +101,7 @@
 by (rule bnd_monoI, blast+)
 
 lemma rtrancl_mono: "r<=s \<Longrightarrow> r^* \<subseteq> s^*"
-apply (unfold rtrancl_def)
+  unfolding rtrancl_def
 apply (rule lfp_mono)
 apply (rule rtrancl_bnd_mono)+
 apply blast
@@ -172,7 +172,7 @@
 
 (*transitivity of transitive closure\<And>-- by induction.*)
 lemma trans_rtrancl: "trans(r^*)"
-apply (unfold trans_def)
+  unfolding trans_def
 apply (intro allI impI)
 apply (erule_tac b = z in rtrancl_induct, assumption)
 apply (blast intro: rtrancl_into_rtrancl)
@@ -208,13 +208,13 @@
 (** Conversions between trancl and rtrancl **)
 
 lemma trancl_into_rtrancl: "\<langle>a,b\<rangle> \<in> r^+ \<Longrightarrow> \<langle>a,b\<rangle> \<in> r^*"
-apply (unfold trancl_def)
+  unfolding trancl_def
 apply (blast intro: rtrancl_into_rtrancl)
 done
 
 (*r^+ contains all pairs in r  *)
 lemma r_into_trancl: "\<langle>a,b\<rangle> \<in> r \<Longrightarrow> \<langle>a,b\<rangle> \<in> r^+"
-apply (unfold trancl_def)
+  unfolding trancl_def
 apply (blast intro!: rtrancl_refl)
 done
 
@@ -266,7 +266,7 @@
 done
 
 lemma trancl_type: "r^+ \<subseteq> field(r)*field(r)"
-apply (unfold trancl_def)
+  unfolding trancl_def
 apply (blast elim: rtrancl_type [THEN subsetD, THEN SigmaE2])
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/UNITY/AllocBase.thy
--- a/src/ZF/UNITY/AllocBase.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/AllocBase.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -118,7 +118,7 @@
 done
 
 lemma mono_tokens [iff]: "mono1(list(A), prefix(A), nat, Le,tokens)"
-apply (unfold mono1_def)
+  unfolding mono1_def
 apply (auto intro: tokens_mono simp add: Le_def)
 done
 
@@ -280,7 +280,7 @@
 lemma all_distinct_Cons [simp]: 
     "all_distinct(Cons(a,l)) \<longleftrightarrow>  
       (a\<in>set_of_list(l) \<longrightarrow> False) \<and> (a \<notin> set_of_list(l) \<longrightarrow> all_distinct(l))"
-apply (unfold all_distinct_def)
+  unfolding all_distinct_def
 apply (auto elim: list.cases)
 done
 
@@ -336,14 +336,14 @@
 
 lemma var_infinite_lemma: 
   "(\<lambda>x\<in>nat. nat_var_inj(x))\<in>inj(nat, var)"
-apply (unfold nat_var_inj_def)
+  unfolding nat_var_inj_def
 apply (rule_tac d = var_inj in lam_injective)
 apply (auto simp add: var.intros nat_list_inj_type)
 apply (simp add: length_nat_list_inj)
 done
 
 lemma nat_lepoll_var: "nat \<lesssim> var"
-apply (unfold lepoll_def)
+  unfolding lepoll_def
 apply (rule_tac x = " (\<lambda>x\<in>nat. nat_var_inj (x))" in exI)
 apply (rule var_infinite_lemma)
 done
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/UNITY/AllocImpl.thy
--- a/src/ZF/UNITY/AllocImpl.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/AllocImpl.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -50,12 +50,12 @@
 
 
 lemma available_tok_value_type [simp,TC]: "s\<in>state \<Longrightarrow> s`available_tok \<in> nat"
-apply (unfold state_def)
+  unfolding state_def
 apply (drule_tac a = available_tok in apply_type, auto)
 done
 
 lemma NbR_value_type [simp,TC]: "s\<in>state \<Longrightarrow> s`NbR \<in> nat"
-apply (unfold state_def)
+  unfolding state_def
 apply (drule_tac a = NbR in apply_type, auto)
 done
 
@@ -270,7 +270,7 @@
             {s\<in>state . k \<le> length(s ` rel)} \<inter> {s\<in>state . s ` NbR = n}
                \<longmapsto>w {x \<in> state. k \<le> length(x`rel)} \<inter>
                  (\<Union>m \<in> greater_than(n). {x \<in> state. x ` NbR=m})"
-apply (unfold greater_than_def)
+  unfolding greater_than_def
 apply (rule_tac A' = "{x \<in> state. k \<le> length(x`rel)} \<inter> {x \<in> state. n < x`NbR}"
        in LeadsTo_weaken_R)
 apply safe
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/UNITY/ClientImpl.thy
--- a/src/ZF/UNITY/ClientImpl.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/ClientImpl.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -56,29 +56,29 @@
 (* This part should be automated *)
 
 lemma ask_value_type [simp,TC]: "s \<in> state \<Longrightarrow> s`ask \<in> list(nat)"
-apply (unfold state_def)
+  unfolding state_def
 apply (drule_tac a = ask in apply_type, auto)
 done
 
 lemma giv_value_type [simp,TC]: "s \<in> state \<Longrightarrow> s`giv \<in> list(nat)"
-apply (unfold state_def)
+  unfolding state_def
 apply (drule_tac a = giv in apply_type, auto)
 done
 
 lemma rel_value_type [simp,TC]: "s \<in> state \<Longrightarrow> s`rel \<in> list(nat)"
-apply (unfold state_def)
+  unfolding state_def
 apply (drule_tac a = rel in apply_type, auto)
 done
 
 lemma tok_value_type [simp,TC]: "s \<in> state \<Longrightarrow> s`tok \<in> nat"
-apply (unfold state_def)
+  unfolding state_def
 apply (drule_tac a = tok in apply_type, auto)
 done
 
 (** The Client Program **)
 
 lemma client_type [simp,TC]: "client_prog \<in> program"
-apply (unfold client_prog_def)
+  unfolding client_prog_def
 apply (simp (no_asm))
 done
 
@@ -118,7 +118,7 @@
 (*Safety property 1 \<in> ask, rel are increasing: (24) *)
 lemma client_prog_Increasing_ask_rel:
 "client_prog: program guarantees Incr(lift(ask)) \<inter> Incr(lift(rel))"
-apply (unfold guar_def)
+  unfolding guar_def
 apply (auto intro!: increasing_imp_Increasing
             simp add: client_prog_ok_iff Increasing.increasing_def preserves_imp_prefix)
 apply (safety, force, force)+
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/UNITY/Comp.thy
--- a/src/ZF/UNITY/Comp.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/Comp.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -68,13 +68,13 @@
 done
 
 lemma component_SKIP [simp]: "F \<in> program \<Longrightarrow> SKIP component F"
-apply (unfold component_def)
+  unfolding component_def
 apply (rule_tac x = F in exI)
 apply (force intro: Join_SKIP_left)
 done
 
 lemma component_refl [simp]: "F \<in> program \<Longrightarrow> F component F"
-apply (unfold component_def)
+  unfolding component_def
 apply (rule_tac x = F in exI)
 apply (force intro: Join_SKIP_right)
 done
@@ -88,7 +88,7 @@
 by (unfold component_def, blast)
 
 lemma component_Join2: "G component (F \<squnion> G)"
-apply (unfold component_def)
+  unfolding component_def
 apply (simp (no_asm) add: Join_commute)
 apply blast
 done
@@ -111,12 +111,12 @@
 done
 
 lemma component_JOIN: "i \<in> I \<Longrightarrow> F(i) component (\<Squnion>i \<in> I. (F(i)))"
-apply (unfold component_def)
+  unfolding component_def
 apply (blast intro: JOIN_absorb)
 done
 
 lemma component_trans: "\<lbrakk>F component G; G component H\<rbrakk> \<Longrightarrow> F component H"
-apply (unfold component_def)
+  unfolding component_def
 apply (blast intro: Join_assoc [symmetric])
 done
 
@@ -175,7 +175,7 @@
 by (auto simp add: preserves_def INT_iff)
 
 lemma fun_pair_apply [simp]: "fun_pair(f,g,x) = <f(x), g(x)>"
-apply (unfold fun_pair_def)
+  unfolding fun_pair_def
 apply (simp (no_asm))
 done
 
@@ -252,7 +252,7 @@
 
 (* component_of satisfies many of component's properties *)
 lemma component_of_refl [simp]: "F \<in> program \<Longrightarrow> F component_of F"
-apply (unfold component_of_def)
+  unfolding component_of_def
 apply (rule_tac x = SKIP in exI, auto)
 done
 
@@ -263,7 +263,7 @@
 
 lemma component_of_trans: 
      "\<lbrakk>F component_of G; G component_of H\<rbrakk> \<Longrightarrow> F component_of H"
-apply (unfold component_of_def)
+  unfolding component_of_def
 apply (blast intro: Join_assoc [symmetric])
 done
 
@@ -276,7 +276,7 @@
 
 lemma localize_AllowedActs_eq [simp]: 
  "AllowedActs(localize(v,F)) = AllowedActs(F) \<inter> (\<Union>G \<in> preserves(v). Acts(G))"
-apply (unfold localize_def)
+  unfolding localize_def
 apply (rule equalityI)
 apply (auto dest: Acts_type [THEN subsetD])
 done
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/UNITY/Constrains.thy
--- a/src/ZF/UNITY/Constrains.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/Constrains.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -66,7 +66,7 @@
 done
 
 lemma st_set_reachable: "st_set(reachable(F))"
-apply (unfold st_set_def)
+  unfolding st_set_def
 apply (rule reachable_type)
 done
 declare st_set_reachable [iff]
@@ -129,7 +129,7 @@
 (*Resembles the previous definition of Constrains*)
 lemma Constrains_eq_constrains: 
 "A Co B = {F \<in> program. F:(reachable(F) \<inter> A) co (reachable(F)  \<inter>  B)}"
-apply (unfold Constrains_def)
+  unfolding Constrains_def
 apply (blast dest: constrains_reachable_Int constrains_type [THEN subsetD]
              intro: constrains_weaken)
 done
@@ -137,7 +137,7 @@
 lemmas Constrains_def2 = Constrains_eq_constrains [THEN eq_reflection]
 
 lemma constrains_imp_Constrains: "F \<in> A co A' \<Longrightarrow> F \<in> A Co A'"
-apply (unfold Constrains_def)
+  unfolding Constrains_def
 apply (blast intro: constrains_weaken_L dest: constrainsD2)
 done
 
@@ -160,26 +160,26 @@
 declare Constrains_empty [iff]
 
 lemma Constrains_state: "F \<in> A Co state \<longleftrightarrow> F \<in> program"
-apply (unfold Constrains_def)
+  unfolding Constrains_def
 apply (auto dest: Constrains_type [THEN subsetD] intro: constrains_imp_Constrains)
 done
 declare Constrains_state [iff]
 
 lemma Constrains_weaken_R: 
         "\<lbrakk>F \<in> A Co A'; A'<=B'\<rbrakk> \<Longrightarrow> F \<in> A Co B'"
-apply (unfold Constrains_def2)
+  unfolding Constrains_def2
 apply (blast intro: constrains_weaken_R)
 done
 
 lemma Constrains_weaken_L: 
     "\<lbrakk>F \<in> A Co A'; B<=A\<rbrakk> \<Longrightarrow> F \<in> B Co A'"
-apply (unfold Constrains_def2)
+  unfolding Constrains_def2
 apply (blast intro: constrains_weaken_L st_set_subset)
 done
 
 lemma Constrains_weaken: 
    "\<lbrakk>F \<in> A Co A'; B<=A; A'<=B'\<rbrakk> \<Longrightarrow> F \<in> B Co B'"
-apply (unfold Constrains_def2)
+  unfolding Constrains_def2
 apply (blast intro: constrains_weaken st_set_subset)
 done
 
@@ -202,7 +202,7 @@
 
 lemma Constrains_Int: 
     "\<lbrakk>F \<in> A Co A'; F \<in> B Co B'\<rbrakk>\<Longrightarrow> F:(A \<inter> B) Co (A' \<inter> B')"
-apply (unfold Constrains_def)
+  unfolding Constrains_def
 apply (subgoal_tac "reachable (F) \<inter> (A \<inter> B) = (reachable (F) \<inter> A) \<inter> (reachable (F) \<inter> B) ")
 apply (auto intro: constrains_Int)
 done
@@ -216,19 +216,19 @@
 done
 
 lemma Constrains_imp_subset: "F \<in> A Co A' \<Longrightarrow> reachable(F) \<inter> A \<subseteq> A'"
-apply (unfold Constrains_def)
+  unfolding Constrains_def
 apply (blast dest: constrains_imp_subset)
 done
 
 lemma Constrains_trans: 
  "\<lbrakk>F \<in> A Co B; F \<in> B Co C\<rbrakk> \<Longrightarrow> F \<in> A Co C"
-apply (unfold Constrains_def2)
+  unfolding Constrains_def2
 apply (blast intro: constrains_trans constrains_weaken)
 done
 
 lemma Constrains_cancel: 
 "\<lbrakk>F \<in> A Co (A' \<union> B); F \<in> B Co B'\<rbrakk> \<Longrightarrow> F \<in> A Co (A' \<union> B')"
-apply (unfold Constrains_def2)
+  unfolding Constrains_def2
 apply (simp (no_asm_use) add: Int_Un_distrib)
 apply (blast intro: constrains_cancel)
 done
@@ -259,27 +259,27 @@
 
 lemma Stable_Un: 
     "\<lbrakk>F \<in> Stable(A); F \<in> Stable(A')\<rbrakk> \<Longrightarrow> F \<in> Stable(A \<union> A')"
-apply (unfold Stable_def)
+  unfolding Stable_def
 apply (blast intro: Constrains_Un)
 done
 
 lemma Stable_Int: 
     "\<lbrakk>F \<in> Stable(A); F \<in> Stable(A')\<rbrakk> \<Longrightarrow> F \<in> Stable (A \<inter> A')"
-apply (unfold Stable_def)
+  unfolding Stable_def
 apply (blast intro: Constrains_Int)
 done
 
 lemma Stable_Constrains_Un: 
     "\<lbrakk>F \<in> Stable(C); F \<in> A Co (C \<union> A')\<rbrakk>    
      \<Longrightarrow> F \<in> (C \<union> A) Co (C \<union> A')"
-apply (unfold Stable_def)
+  unfolding Stable_def
 apply (blast intro: Constrains_Un [THEN Constrains_weaken_R])
 done
 
 lemma Stable_Constrains_Int: 
     "\<lbrakk>F \<in> Stable(C); F \<in> (C \<inter> A) Co A'\<rbrakk>    
      \<Longrightarrow> F \<in> (C \<inter> A) Co (C \<inter> A')"
-apply (unfold Stable_def)
+  unfolding Stable_def
 apply (blast intro: Constrains_Int [THEN Constrains_weaken])
 done
 
@@ -302,7 +302,7 @@
 done
 
 lemma Stable_type: "Stable(A) \<subseteq> program"
-apply (unfold Stable_def)
+  unfolding Stable_def
 apply (rule Constrains_type)
 done
 
@@ -329,7 +329,7 @@
 (** Unless **)
 
 lemma Unless_type: "A Unless B <=program"
-apply (unfold op_Unless_def)
+  unfolding op_Unless_def
 apply (rule Constrains_type)
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/UNITY/Distributor.thy
--- a/src/ZF/UNITY/Distributor.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/Distributor.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -55,19 +55,19 @@
 
 
 lemma (in distr) In_value_type [simp,TC]: "s \<in> state \<Longrightarrow> s`In \<in> list(A)"
-apply (unfold state_def)
+  unfolding state_def
 apply (drule_tac a = In in apply_type, auto)
 done
 
 lemma (in distr) iIn_value_type [simp,TC]:
      "s \<in> state \<Longrightarrow> s`iIn \<in> list(nat)"
-apply (unfold state_def)
+  unfolding state_def
 apply (drule_tac a = iIn in apply_type, auto)
 done
 
 lemma (in distr) Out_value_type [simp,TC]:
      "s \<in> state \<Longrightarrow> s`Out(n):list(A)"
-apply (unfold state_def)
+  unfolding state_def
 apply (drule_tac a = "Out (n)" in apply_type)
 apply auto
 done
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/UNITY/FP.thy
--- a/src/ZF/UNITY/FP.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/FP.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -24,7 +24,7 @@
 by (unfold FP_Orig_def, blast)
 
 lemma st_set_FP_Orig [iff]: "st_set(FP_Orig(F))"
-apply (unfold st_set_def)
+  unfolding st_set_def
 apply (rule FP_Orig_type)
 done
 
@@ -32,7 +32,7 @@
 by (unfold FP_def, blast)
 
 lemma st_set_FP [iff]: "st_set(FP(F))"
-apply (unfold st_set_def)
+  unfolding st_set_def
 apply (rule FP_type)
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/UNITY/Follows.thy
--- a/src/ZF/UNITY/Follows.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/Follows.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -165,7 +165,7 @@
 
 (* Follows type *)
 lemma Follows_type: "Follows(A, r, f, g)<=program"
-apply (unfold Follows_def)
+  unfolding Follows_def
 apply (blast dest: Increasing_type [THEN subsetD])
 done
 
@@ -175,7 +175,7 @@
 lemma FollowsD:
 "F \<in> Follows(A, r, f, g)\<Longrightarrow>
   F \<in> program \<and> (\<exists>a. a \<in> A) \<and> (\<forall>x \<in> state. f(x):A \<and> g(x):A)"
-apply (unfold Follows_def)
+  unfolding Follows_def
 apply (blast dest: IncreasingD)
 done
 
@@ -406,7 +406,7 @@
 
 lemma empty_le_MultLe [simp]:
 "\<lbrakk>multiset(M); mset_of(M)<= A\<rbrakk> \<Longrightarrow> \<langle>0, M\<rangle> \<in> MultLe(A, r)"
-apply (unfold MultLe_def)
+  unfolding MultLe_def
 apply (case_tac "M=0")
 apply (auto simp add: FiniteFun.intros)
 apply (subgoal_tac "<0 +# 0, 0 +# M> \<in> multirel (A, r - id (A))")
@@ -420,7 +420,7 @@
 lemma munion_mono:
 "\<lbrakk>\<langle>M, N\<rangle> \<in> MultLe(A, r); \<langle>K, L\<rangle> \<in> MultLe(A, r)\<rbrakk> \<Longrightarrow>
   <M +# K, N +# L> \<in> MultLe(A, r)"
-apply (unfold MultLe_def)
+  unfolding MultLe_def
 apply (auto intro: munion_multirel_mono1 munion_multirel_mono2
        munion_multirel_mono multiset_into_Mult simp add: Mult_iff_multiset)
 done
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/UNITY/GenPrefix.thy
--- a/src/ZF/UNITY/GenPrefix.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/GenPrefix.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -182,7 +182,7 @@
 lemma prefix_gen_prefix_trans:
     "\<lbrakk>\<langle>x,y\<rangle> \<in> prefix(A); \<langle>y, z\<rangle> \<in> gen_prefix(A, r); r<=A*A\<rbrakk>
       \<Longrightarrow>  \<langle>x, z\<rangle> \<in> gen_prefix(A, r)"
-apply (unfold prefix_def)
+  unfolding prefix_def
 apply (rule_tac P = "\<lambda>r. \<langle>x,z\<rangle> \<in> gen_prefix (A, r) " in right_comp_id [THEN subst])
 apply (blast dest: gen_prefix_trans_comp gen_prefix.dom_subset [THEN subsetD])+
 done
@@ -191,7 +191,7 @@
 lemma gen_prefix_prefix_trans:
 "\<lbrakk>\<langle>x,y\<rangle> \<in> gen_prefix(A,r); \<langle>y, z\<rangle> \<in> prefix(A); r<=A*A\<rbrakk>
   \<Longrightarrow>  \<langle>x, z\<rangle> \<in> gen_prefix(A, r)"
-apply (unfold prefix_def)
+  unfolding prefix_def
 apply (rule_tac P = "\<lambda>r. \<langle>x,z\<rangle> \<in> gen_prefix (A, r) " in left_comp_id [THEN subst])
 apply (blast dest: gen_prefix_trans_comp gen_prefix.dom_subset [THEN subsetD])+
 done
@@ -232,7 +232,7 @@
 lemma same_gen_prefix_gen_prefix:
  "\<lbrakk>refl(A, r);  xs \<in> list(A)\<rbrakk> \<Longrightarrow>
     <xs@ys, xs@zs>: gen_prefix(A, r) \<longleftrightarrow> \<langle>ys,zs\<rangle> \<in> gen_prefix(A, r)"
-apply (unfold refl_def)
+  unfolding refl_def
 apply (induct_tac "xs")
 apply (simp_all (no_asm_simp))
 done
@@ -338,14 +338,14 @@
 (** prefix is a partial order: **)
 
 lemma refl_prefix: "refl(list(A), prefix(A))"
-apply (unfold prefix_def)
+  unfolding prefix_def
 apply (rule refl_gen_prefix)
 apply (auto simp add: refl_def)
 done
 declare refl_prefix [THEN reflD, simp]
 
 lemma trans_prefix: "trans(prefix(A))"
-apply (unfold prefix_def)
+  unfolding prefix_def
 apply (rule trans_gen_prefix)
 apply (auto simp add: trans_def)
 done
@@ -353,7 +353,7 @@
 lemmas prefix_trans = trans_prefix [THEN transD]
 
 lemma trans_on_prefix: "trans[list(A)](prefix(A))"
-apply (unfold prefix_def)
+  unfolding prefix_def
 apply (rule trans_on_gen_prefix)
 apply (auto simp add: trans_def)
 done
@@ -365,7 +365,7 @@
 lemma set_of_list_prefix_mono:
 "\<langle>xs,ys\<rangle> \<in> prefix(A) \<Longrightarrow> set_of_list(xs) \<subseteq> set_of_list(ys)"
 
-apply (unfold prefix_def)
+  unfolding prefix_def
 apply (erule gen_prefix.induct)
 apply (subgoal_tac [3] "xs \<in> list (A) \<and>ys \<in> list (A) ")
 prefer 4 apply (blast dest: gen_prefix.dom_subset [THEN subsetD])
@@ -376,7 +376,7 @@
 
 lemma Nil_prefix: "xs \<in> list(A) \<Longrightarrow> <[],xs> \<in> prefix(A)"
 
-apply (unfold prefix_def)
+  unfolding prefix_def
 apply (simp (no_asm_simp) add: Nil_gen_prefix)
 done
 declare Nil_prefix [simp]
@@ -399,7 +399,7 @@
 
 lemma same_prefix_prefix:
 "xs \<in> list(A)\<Longrightarrow> <xs@ys,xs@zs> \<in> prefix(A) \<longleftrightarrow> (\<langle>ys,zs\<rangle> \<in> prefix(A))"
-apply (unfold prefix_def)
+  unfolding prefix_def
 apply (subgoal_tac "refl (A,id (A))")
 apply (simp (no_asm_simp))
 apply (auto simp add: refl_def)
@@ -414,7 +414,7 @@
 
 lemma prefix_appendI:
 "\<lbrakk>\<langle>xs,ys\<rangle> \<in> prefix(A); zs \<in> list(A)\<rbrakk> \<Longrightarrow> <xs,ys@zs> \<in> prefix(A)"
-apply (unfold prefix_def)
+  unfolding prefix_def
 apply (erule gen_prefix.append, assumption)
 done
 declare prefix_appendI [simp]
@@ -423,14 +423,14 @@
 "\<lbrakk>xs \<in> list(A); ys \<in> list(A); y \<in> A\<rbrakk> \<Longrightarrow>
   <xs,Cons(y,ys)> \<in> prefix(A) \<longleftrightarrow>
   (xs=[] | (\<exists>zs. xs=Cons(y,zs) \<and> \<langle>zs,ys\<rangle> \<in> prefix(A)))"
-apply (unfold prefix_def)
+  unfolding prefix_def
 apply (auto simp add: gen_prefix_Cons)
 done
 
 lemma append_one_prefix:
   "\<lbrakk>\<langle>xs,ys\<rangle> \<in> prefix(A); length(xs) < length(ys)\<rbrakk>
   \<Longrightarrow> <xs @ [nth(length(xs),ys)], ys> \<in> prefix(A)"
-apply (unfold prefix_def)
+  unfolding prefix_def
 apply (subgoal_tac "refl (A, id (A))")
 apply (simp (no_asm_simp) add: append_one_gen_prefix)
 apply (auto simp add: refl_def)
@@ -438,24 +438,24 @@
 
 lemma prefix_length_le:
 "\<langle>xs,ys\<rangle> \<in> prefix(A) \<Longrightarrow> length(xs) \<le> length(ys)"
-apply (unfold prefix_def)
+  unfolding prefix_def
 apply (blast dest: gen_prefix_length_le)
 done
 
 lemma prefix_type: "prefix(A)<=list(A)*list(A)"
-apply (unfold prefix_def)
+  unfolding prefix_def
 apply (blast intro!: gen_prefix.dom_subset)
 done
 
 lemma strict_prefix_type:
 "strict_prefix(A) \<subseteq> list(A)*list(A)"
-apply (unfold strict_prefix_def)
+  unfolding strict_prefix_def
 apply (blast intro!: prefix_type [THEN subsetD])
 done
 
 lemma strict_prefix_length_lt_aux:
      "\<langle>xs,ys\<rangle> \<in> prefix(A) \<Longrightarrow> xs\<noteq>ys \<longrightarrow> length(xs) < length(ys)"
-apply (unfold prefix_def)
+  unfolding prefix_def
 apply (erule gen_prefix.induct, clarify)
 apply (subgoal_tac [!] "ys \<in> list(A) \<and> xs \<in> list(A)")
 apply (auto dest: gen_prefix.dom_subset [THEN subsetD]
@@ -468,7 +468,7 @@
 
 lemma strict_prefix_length_lt:
      "\<langle>xs,ys\<rangle>:strict_prefix(A) \<Longrightarrow> length(xs) < length(ys)"
-apply (unfold strict_prefix_def)
+  unfolding strict_prefix_def
 apply (rule strict_prefix_length_lt_aux [THEN mp])
 apply (auto dest: prefix_type [THEN subsetD])
 done
@@ -476,7 +476,7 @@
 (*Equivalence to the definition used in Lex/Prefix.thy*)
 lemma prefix_iff:
     "\<langle>xs,zs\<rangle> \<in> prefix(A) \<longleftrightarrow> (\<exists>ys \<in> list(A). zs = xs@ys) \<and> xs \<in> list(A)"
-apply (unfold prefix_def)
+  unfolding prefix_def
 apply (auto simp add: gen_prefix_iff_nth lt_nat_in_nat nth_append nth_type app_type length_app)
 apply (subgoal_tac "drop (length (xs), zs) \<in> list (A) ")
 apply (rule_tac x = "drop (length (xs), zs) " in bexI)
@@ -544,7 +544,7 @@
 declare refl_Le [simp]
 
 lemma antisym_Le: "antisym(Le)"
-apply (unfold antisym_def)
+  unfolding antisym_def
 apply (auto intro: le_anti_sym)
 done
 declare antisym_Le [simp]
@@ -579,7 +579,7 @@
 lemma prefix_imp_pfixLe:
 "\<langle>xs,ys\<rangle>:prefix(nat)\<Longrightarrow> xs pfixLe ys"
 
-apply (unfold prefix_def)
+  unfolding prefix_def
 apply (rule gen_prefix_mono [THEN subsetD], auto)
 done
 
@@ -619,7 +619,7 @@
 lemma prefix_imp_take:
 "\<langle>xs, ys\<rangle> \<in> prefix(A) \<Longrightarrow> xs = take(length(xs), ys)"
 
-apply (unfold prefix_def)
+  unfolding prefix_def
 apply (erule gen_prefix.induct)
 apply (subgoal_tac [3] "length (xs) :nat")
 apply (auto dest: gen_prefix.dom_subset [THEN subsetD] simp add: length_type)
@@ -641,7 +641,7 @@
 by (blast intro: prefix_length_equal le_anti_sym prefix_length_le)
 
 lemma take_prefix [rule_format]: "xs \<in> list(A) \<Longrightarrow> \<forall>n \<in> nat. <take(n, xs), xs> \<in> prefix(A)"
-apply (unfold prefix_def)
+  unfolding prefix_def
 apply (erule list.induct, simp, clarify)
 apply (erule natE, auto)
 done
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/UNITY/Guar.thy
--- a/src/ZF/UNITY/Guar.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/Guar.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -95,7 +95,7 @@
 lemma ex1 [rule_format]: 
  "GG \<in> Fin(program) 
   \<Longrightarrow> ex_prop(X) \<longrightarrow> GG \<inter> X\<noteq>0 \<longrightarrow> OK(GG, (\<lambda>G. G)) \<longrightarrow>(\<Squnion>G \<in> GG. G) \<in> X"
-apply (unfold ex_prop_def)
+  unfolding ex_prop_def
 apply (erule Fin_induct)
 apply (simp_all add: OK_cons_iff)
 apply (safe elim!: not_emptyE, auto) 
@@ -132,14 +132,14 @@
 (*** universal properties ***)
 
 lemma uv_imp_subset_program: "uv_prop(X)\<Longrightarrow> X\<subseteq>program"
-apply (unfold uv_prop_def)
+  unfolding uv_prop_def
 apply (simp (no_asm_simp))
 done
 
 lemma uv1 [rule_format]: 
      "GG \<in> Fin(program) \<Longrightarrow>  
       (uv_prop(X)\<longrightarrow> GG \<subseteq> X \<and> OK(GG, (\<lambda>G. G)) \<longrightarrow> (\<Squnion>G \<in> GG. G) \<in> X)"
-apply (unfold uv_prop_def)
+  unfolding uv_prop_def
 apply (erule Fin_induct)
 apply (auto simp add: OK_cons_iff)
 done
@@ -216,7 +216,7 @@
 done
 
 lemma guarantees_imp: "(Y = program guarantees Y) \<Longrightarrow> ex_prop(Y)"
-apply (unfold guar_def)
+  unfolding guar_def
 apply (simp (no_asm_simp) add: ex_prop_equiv)
 apply safe
 apply (blast intro: elim: equalityE) 
@@ -231,7 +231,7 @@
 
 lemma guarantees_UN_left: 
      "i \<in> I \<Longrightarrow>(\<Union>i \<in> I. X(i)) guarantees Y = (\<Inter>i \<in> I. X(i) guarantees Y)"
-apply (unfold guar_def)
+  unfolding guar_def
 apply (rule equalityI, safe)
  prefer 2 apply force
 apply blast+
@@ -239,13 +239,13 @@
 
 lemma guarantees_Un_left: 
      "(X \<union> Y) guarantees Z = (X guarantees Z) \<inter> (Y guarantees Z)"
-apply (unfold guar_def)
+  unfolding guar_def
 apply (rule equalityI, safe, blast+)
 done
 
 lemma guarantees_INT_right: 
      "i \<in> I \<Longrightarrow> X guarantees (\<Inter>i \<in> I. Y(i)) = (\<Inter>i \<in> I. X guarantees Y(i))"
-apply (unfold guar_def)
+  unfolding guar_def
 apply (rule equalityI, safe, blast+)
 done
 
@@ -307,7 +307,7 @@
     "\<lbrakk>F \<in> U guarantees V;  G \<in> X guarantees Y; F ok G\<rbrakk>  
      \<Longrightarrow> F \<squnion> G: (U \<inter> X) guarantees (V \<inter> Y)"
 
-apply (unfold guar_def)
+  unfolding guar_def
 apply (simp (no_asm))
 apply safe
 apply (simp add: Join_assoc)
@@ -319,7 +319,7 @@
 lemma guarantees_Join_Un: 
     "\<lbrakk>F \<in> U guarantees V;  G \<in> X guarantees Y; F ok G\<rbrakk>   
      \<Longrightarrow> F \<squnion> G: (U \<union> X) guarantees (V \<union> Y)"
-apply (unfold guar_def)
+  unfolding guar_def
 apply (simp (no_asm))
 apply safe
 apply (simp add: Join_assoc)
@@ -480,7 +480,7 @@
 
 lemma wx_equiv: 
      "wx(X) = {F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> (F \<squnion> G) \<in> X}"
-apply (unfold wx_def)
+  unfolding wx_def
 apply (rule equalityI, safe, blast)
  apply (simp (no_asm_use) add: ex_prop_def)
 apply blast 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/UNITY/Increasing.thy
--- a/src/ZF/UNITY/Increasing.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/Increasing.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -41,7 +41,7 @@
 
 lemma increasingD: 
 "F \<in> increasing[A](r,f) \<Longrightarrow> F \<in> program \<and> (\<exists>a. a \<in> A) \<and> (\<forall>s \<in> state. f(s):A)"
-apply (unfold increasing_def)
+  unfolding increasing_def
 apply (subgoal_tac "\<exists>x. x \<in> state")
 apply (auto dest: stable_type [THEN subsetD] intro: st0_in_state)
 done
@@ -110,7 +110,7 @@
 
 lemma IncreasingD: 
 "F \<in> Increasing[A](r, f) \<Longrightarrow> F \<in> program \<and> (\<exists>a. a \<in> A) \<and> (\<forall>s \<in> state. f(s):A)"
-apply (unfold Increasing_def)
+  unfolding Increasing_def
 apply (subgoal_tac "\<exists>x. x \<in> state")
 apply (auto intro: st0_in_state)
 done
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/UNITY/Merge.thy
--- a/src/ZF/UNITY/Merge.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/Merge.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -85,18 +85,18 @@
 
 
 lemma (in merge) In_value_type [TC,simp]: "s \<in> state \<Longrightarrow> s`In(n) \<in> list(A)"
-apply (unfold state_def)
+  unfolding state_def
 apply (drule_tac a = "In (n)" in apply_type)
 apply auto
 done
 
 lemma (in merge) Out_value_type [TC,simp]: "s \<in> state \<Longrightarrow> s`Out \<in> list(A)"
-apply (unfold state_def)
+  unfolding state_def
 apply (drule_tac a = Out in apply_type, auto)
 done
 
 lemma (in merge) iOut_value_type [TC,simp]: "s \<in> state \<Longrightarrow> s`iOut \<in> list(nat)"
-apply (unfold state_def)
+  unfolding state_def
 apply (drule_tac a = iOut in apply_type, auto)
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/UNITY/Monotonicity.thy
--- a/src/ZF/UNITY/Monotonicity.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/Monotonicity.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -95,7 +95,7 @@
 
 lemma mono_length [iff]:
      "mono1(list(A), prefix(A), nat, Le, length)"
-apply (unfold mono1_def)
+  unfolding mono1_def
 apply (auto dest: prefix_length_le simp add: Le_def)
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/UNITY/Mutex.thy
--- a/src/ZF/UNITY/Mutex.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/Mutex.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -94,27 +94,27 @@
 declare p_type [simp] u_type [simp] v_type [simp] m_type [simp] n_type [simp]
 
 lemma u_value_type: "s \<in> state \<Longrightarrow>s`u \<in> bool"
-apply (unfold state_def)
+  unfolding state_def
 apply (drule_tac a = u in apply_type, auto)
 done
 
 lemma v_value_type: "s \<in> state \<Longrightarrow> s`v \<in> bool"
-apply (unfold state_def)
+  unfolding state_def
 apply (drule_tac a = v in apply_type, auto)
 done
 
 lemma p_value_type: "s \<in> state \<Longrightarrow> s`p \<in> bool"
-apply (unfold state_def)
+  unfolding state_def
 apply (drule_tac a = p in apply_type, auto)
 done
 
 lemma m_value_type: "s \<in> state \<Longrightarrow> s`m \<in> int"
-apply (unfold state_def)
+  unfolding state_def
 apply (drule_tac a = m in apply_type, auto)
 done
 
 lemma n_value_type: "s \<in> state \<Longrightarrow>s`n \<in> int"
-apply (unfold state_def)
+  unfolding state_def
 apply (drule_tac a = n in apply_type, auto)
 done
 
@@ -216,7 +216,7 @@
 
 lemma U_F3: "Mutex \<in> {s \<in> state. s`m = #3} \<longmapsto>w {s \<in> state. s`p=1}"
 apply (rule_tac B = "{s \<in> state. s`m = #4}" in LeadsTo_Trans)
- apply (unfold Mutex_def)
+   unfolding Mutex_def
  apply (ensures U3)
 apply (ensures U4)
 done
@@ -267,7 +267,7 @@
 
 lemma V_F3: "Mutex \<in> {s \<in> state. s`n = #3} \<longmapsto>w {s \<in> state. s`p=0}"
 apply (rule_tac B = "{s \<in> state. s`n = #4}" in LeadsTo_Trans)
- apply (unfold Mutex_def)
+   unfolding Mutex_def
  apply (ensures V3)
 apply (ensures V4)
 done
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/UNITY/SubstAx.thy
--- a/src/ZF/UNITY/SubstAx.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/SubstAx.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -26,7 +26,7 @@
 (* Equivalence with the HOL-like definition *)
 lemma LeadsTo_eq:
 "st_set(B)\<Longrightarrow> A \<longmapsto>w B = {F \<in> program. F:(reachable(F) \<inter> A) \<longmapsto> B}"
-apply (unfold LeadsTo_def)
+  unfolding LeadsTo_def
 apply (blast dest: psp_stable2 leadsToD2 constrainsD2 intro: leadsTo_weaken)
 done
 
@@ -40,7 +40,7 @@
 by (simp add: LeadsTo_def Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric] leadsToD2)
 
 lemma Always_LeadsTo_post: "F \<in> Always(I) \<Longrightarrow> (F \<in> A \<longmapsto>w (I \<inter> A')) \<longleftrightarrow> (F \<in> A \<longmapsto>w A')"
-apply (unfold LeadsTo_def)
+  unfolding LeadsTo_def
 apply (simp add: Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric] leadsToD2)
 done
 
@@ -123,12 +123,12 @@
 declare LeadsTo_state [iff]
 
 lemma LeadsTo_weaken_R: "\<lbrakk>F \<in> A \<longmapsto>w A';  A'<=B'\<rbrakk> \<Longrightarrow> F \<in> A \<longmapsto>w B'"
-apply (unfold LeadsTo_def)
+  unfolding LeadsTo_def
 apply (auto intro: leadsTo_weaken_R)
 done
 
 lemma LeadsTo_weaken_L: "\<lbrakk>F \<in> A \<longmapsto>w A'; B \<subseteq> A\<rbrakk> \<Longrightarrow> F \<in> B \<longmapsto>w A'"
-apply (unfold LeadsTo_def)
+  unfolding LeadsTo_def
 apply (auto intro: leadsTo_weaken_L)
 done
 
@@ -256,7 +256,7 @@
 
 lemma PSP_Unless:
 "\<lbrakk>F \<in> A \<longmapsto>w A'; F \<in> B Unless B'\<rbrakk>\<Longrightarrow> F:(A \<inter> B) \<longmapsto>w ((A' \<inter> B) \<union> B')"
-apply (unfold op_Unless_def)
+  unfolding op_Unless_def
 apply (drule PSP, assumption)
 apply (blast intro: LeadsTo_Diff LeadsTo_weaken subset_imp_LeadsTo)
 done
@@ -327,7 +327,7 @@
      "\<lbrakk>F \<in> A \<longmapsto>w A';  F \<in> Stable(A');
          F \<in> B \<longmapsto>w B';  F \<in> Stable(B')\<rbrakk>
     \<Longrightarrow> F \<in> (A \<inter> B) \<longmapsto>w (A' \<inter> B')"
-apply (unfold Stable_def)
+  unfolding Stable_def
 apply (rule_tac C1 = 0 in Completion [THEN LeadsTo_weaken_R])
     prefer 5
     apply blast
@@ -339,7 +339,7 @@
          (\<And>i. i \<in> I \<Longrightarrow> F \<in> A(i) \<longmapsto>w A'(i));
          (\<And>i. i \<in> I \<Longrightarrow>F \<in> Stable(A'(i)));   F \<in> program\<rbrakk>
       \<Longrightarrow> F \<in> (\<Inter>i \<in> I. A(i)) \<longmapsto>w (\<Inter>i \<in> I. A'(i))"
-apply (unfold Stable_def)
+  unfolding Stable_def
 apply (rule_tac C1 = 0 in Finite_completion [THEN LeadsTo_weaken_R], simp_all)
 apply (rule_tac [3] subset_refl, auto)
 done
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/UNITY/UNITY.thy
--- a/src/ZF/UNITY/UNITY.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/UNITY.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -165,7 +165,7 @@
 lemmas InitD = Init_type [THEN subsetD]
 
 lemma st_set_Init [iff]: "st_set(Init(F))"
-apply (unfold st_set_def)
+  unfolding st_set_def
 apply (rule Init_type)
 done
 
@@ -469,7 +469,7 @@
 by (force simp add: unless_def constrains_def) 
 
 lemma unlessI: "\<lbrakk>F \<in> (A-B) co (A \<union> B)\<rbrakk> \<Longrightarrow> F \<in> A unless B"
-apply (unfold unless_def)
+  unfolding unless_def
 apply (blast dest: constrainsD2)
 done
 
@@ -515,34 +515,34 @@
 
 lemma stable_Un:
     "\<lbrakk>F \<in> stable(A); F \<in> stable(A')\<rbrakk> \<Longrightarrow> F \<in> stable(A \<union> A')"
-apply (unfold stable_def)
+  unfolding stable_def
 apply (blast intro: constrains_Un)
 done
 
 lemma stable_UN:
      "\<lbrakk>\<And>i. i\<in>I \<Longrightarrow> F \<in> stable(A(i)); F \<in> program\<rbrakk> 
       \<Longrightarrow> F \<in> stable (\<Union>i \<in> I. A(i))"
-apply (unfold stable_def)
+  unfolding stable_def
 apply (blast intro: constrains_UN)
 done
 
 lemma stable_Int:
     "\<lbrakk>F \<in> stable(A);  F \<in> stable(A')\<rbrakk> \<Longrightarrow> F \<in> stable (A \<inter> A')"
-apply (unfold stable_def)
+  unfolding stable_def
 apply (blast intro: constrains_Int)
 done
 
 lemma stable_INT:
      "\<lbrakk>\<And>i. i \<in> I \<Longrightarrow> F \<in> stable(A(i)); F \<in> program\<rbrakk>
       \<Longrightarrow> F \<in> stable (\<Inter>i \<in> I. A(i))"
-apply (unfold stable_def)
+  unfolding stable_def
 apply (blast intro: constrains_INT)
 done
 
 lemma stable_All:
     "\<lbrakk>\<forall>z. F \<in> stable({s \<in> state. P(s, z)}); F \<in> program\<rbrakk>
      \<Longrightarrow> F \<in> stable({s \<in> state. \<forall>z. P(s, z)})"
-apply (unfold stable_def)
+  unfolding stable_def
 apply (rule constrains_All, auto)
 done
 
@@ -562,7 +562,7 @@
 subsection\<open>The Operator \<^term>\<open>invariant\<close>\<close>
 
 lemma invariant_type: "invariant(A) \<subseteq> program"
-apply (unfold invariant_def)
+  unfolding invariant_def
 apply (blast dest: stable_type [THEN subsetD])
 done
 
@@ -575,7 +575,7 @@
 by (unfold invariant_def initially_def, auto)
 
 lemma invariantD2: "F \<in> invariant(A) \<Longrightarrow> F \<in> program \<and> st_set(A)"
-apply (unfold invariant_def)
+  unfolding invariant_def
 apply (blast dest: stableD2)
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/UNITY/Union.thy
--- a/src/ZF/UNITY/Union.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/Union.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -159,7 +159,7 @@
 
 lemma Acts_JOIN [simp]:
      "Acts(JOIN(I,F)) = cons(id(state), \<Union>i \<in> I.  Acts(F(i)))"
-apply (unfold JOIN_def)
+  unfolding JOIN_def
 apply (auto simp del: INT_simps UN_simps)
 apply (rule equalityI)
 apply (auto dest: Acts_type [THEN subsetD])
@@ -325,7 +325,7 @@
      "i \<in> I \<Longrightarrow>
       (\<Squnion>i \<in> I. F(i)) \<in> transient(A) \<longleftrightarrow> (\<exists>i \<in> I. programify(F(i)) \<in> transient(A))"
 apply (auto simp add: transient_def JOIN_def)
-apply (unfold st_set_def)
+  unfolding st_set_def
 apply (drule_tac [2] x = act in bspec)
 apply (auto dest: Acts_type [THEN subsetD])
 done
@@ -357,7 +357,7 @@
       (programify(F) \<in> (A-B) co (A \<union> B) \<and> programify(G) \<in> (A-B) co (A \<union> B) \<and>
        (programify(F) \<in>  transient (A-B) | programify(G) \<in> transient (A-B)))"
 
-apply (unfold ensures_def)
+  unfolding ensures_def
 apply (auto simp add: Join_transient)
 done
 
@@ -567,7 +567,7 @@
 lemma def_UNION_ok_iff:
 "\<lbrakk>F \<equiv> mk_program(init,acts, \<Union>G \<in> X. Acts(G)); safety_prop(X)\<rbrakk>
       \<Longrightarrow> F ok G \<longleftrightarrow> (programify(G) \<in> X \<and> acts \<inter> Pow(state*state) \<subseteq> AllowedActs(G))"
-apply (unfold ok_def)
+  unfolding ok_def
 apply (drule_tac G = G in safety_prop_Acts_iff)
 apply (cut_tac F = G in AllowedActs_type)
 apply (cut_tac F = G in Acts_type, auto)
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/UNITY/WFair.thy
--- a/src/ZF/UNITY/WFair.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/UNITY/WFair.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -116,7 +116,7 @@
 
 lemma ensuresI:
 "\<lbrakk>F:(A-B) co (A \<union> B); F \<in> transient(A-B)\<rbrakk>\<Longrightarrow>F \<in> A ensures B"
-apply (unfold ensures_def)
+  unfolding ensures_def
 apply (auto simp add: transient_type [THEN subsetD])
 done
 
@@ -131,7 +131,7 @@
 by (unfold ensures_def, auto)
 
 lemma ensures_weaken_R: "\<lbrakk>F \<in> A ensures A'; A'<=B'\<rbrakk> \<Longrightarrow> F \<in> A ensures B'"
-apply (unfold ensures_def)
+  unfolding ensures_def
 apply (blast intro: transient_strengthen constrains_weaken)
 done
 
@@ -139,7 +139,7 @@
 lemma stable_ensures_Int:
      "\<lbrakk>F \<in> stable(C);  F \<in> A ensures B\<rbrakk> \<Longrightarrow> F:(C \<inter> A) ensures (C \<inter> B)"
 
-apply (unfold ensures_def)
+  unfolding ensures_def
 apply (simp (no_asm) add: Int_Un_distrib [symmetric] Diff_Int_distrib [symmetric])
 apply (blast intro: transient_strengthen stable_constrains_Int constrains_weaken)
 done
@@ -182,13 +182,13 @@
 lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis]
 
 lemma leadsTo_Trans: "\<lbrakk>F \<in> A \<longmapsto> B;  F \<in> B \<longmapsto> C\<rbrakk>\<Longrightarrow>F \<in> A \<longmapsto> C"
-apply (unfold leadsTo_def)
+  unfolding leadsTo_def
 apply (auto intro: leads.Trans)
 done
 
 (* Better when used in association with leadsTo_weaken_R *)
 lemma transient_imp_leadsTo: "F \<in> transient(A) \<Longrightarrow> F \<in> A \<longmapsto> (state-A)"
-apply (unfold transient_def)
+  unfolding transient_def
 apply (blast intro: ensuresI [THEN leadsTo_Basis] constrains_weaken transientI)
 done
 
@@ -424,7 +424,7 @@
 
 lemma psp_stable:
    "\<lbrakk>F \<in> A \<longmapsto> A'; F \<in> stable(B)\<rbrakk> \<Longrightarrow> F:(A \<inter> B) \<longmapsto> (A' \<inter> B)"
-apply (unfold stable_def)
+  unfolding stable_def
 apply (frule leadsToD2)
 apply (erule leadsTo_induct)
 prefer 3 apply (blast intro: leadsTo_Union_Int)
@@ -470,7 +470,7 @@
 lemma psp_unless:
    "\<lbrakk>F \<in> A \<longmapsto> A';  F \<in> B unless B'; st_set(B); st_set(B')\<rbrakk>
     \<Longrightarrow> F \<in> (A \<inter> B) \<longmapsto> ((A' \<inter> B) \<union> B')"
-apply (unfold unless_def)
+  unfolding unless_def
 apply (subgoal_tac "st_set (A) \<and>st_set (A') ")
 prefer 2 apply (blast dest: leadsToD2)
 apply (drule psp, assumption, blast)
@@ -511,7 +511,7 @@
 done
 
 lemma nat_measure_field: "field(measure(nat, \<lambda>x. x)) = nat"
-apply (unfold field_def)
+  unfolding field_def
 apply (simp add: measure_def)
 apply (rule equalityI, force, clarify)
 apply (erule_tac V = "x\<notin>range (y)" for y in thin_rl)
@@ -551,13 +551,13 @@
 by (unfold wlt_def, auto)
 
 lemma wlt_st_set: "st_set(wlt(F, B))"
-apply (unfold st_set_def)
+  unfolding st_set_def
 apply (rule wlt_type)
 done
 declare wlt_st_set [iff]
 
 lemma wlt_leadsTo_iff: "F \<in> wlt(F, B) \<longmapsto> B \<longleftrightarrow> (F \<in> program \<and> st_set(B))"
-apply (unfold wlt_def)
+  unfolding wlt_def
 apply (blast dest: leadsToD2 intro!: leadsTo_Union)
 done
 
@@ -565,7 +565,7 @@
 lemmas wlt_leadsTo = conjI [THEN wlt_leadsTo_iff [THEN iffD2]]
 
 lemma leadsTo_subset: "F \<in> A \<longmapsto> B \<Longrightarrow> A \<subseteq> wlt(F, B)"
-apply (unfold wlt_def)
+  unfolding wlt_def
 apply (frule leadsToD2)
 apply (auto simp add: st_set_def)
 done
@@ -687,7 +687,7 @@
      "\<lbrakk>F \<in> A \<longmapsto> A';  F \<in> stable(A');
          F \<in> B \<longmapsto> B';  F \<in> stable(B')\<rbrakk>
     \<Longrightarrow> F \<in> (A \<inter> B) \<longmapsto> (A' \<inter> B')"
-apply (unfold stable_def)
+  unfolding stable_def
 apply (rule_tac C1 = 0 in completion [THEN leadsTo_weaken_R], simp+)
 apply (blast dest: leadsToD2)
 done
@@ -698,7 +698,7 @@
          (\<And>i. i \<in> I \<Longrightarrow> F \<in> A(i) \<longmapsto> A'(i));
          (\<And>i. i \<in> I \<Longrightarrow> F \<in> stable(A'(i)));  F \<in> program\<rbrakk>
       \<Longrightarrow> F \<in> (\<Inter>i \<in> I. A(i)) \<longmapsto> (\<Inter>i \<in> I. A'(i))"
-apply (unfold stable_def)
+  unfolding stable_def
 apply (subgoal_tac "st_set (\<Inter>i \<in> I. A' (i))")
 prefer 2 apply (blast dest: leadsToD2)
 apply (rule_tac C1 = 0 in finite_completion [THEN leadsTo_weaken_R], auto)
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Univ.thy
--- a/src/ZF/Univ.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Univ.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -125,7 +125,7 @@
 
 lemma Pair_in_Vfrom:
     "\<lbrakk>a \<in> Vfrom(A,i);  b \<in> Vfrom(A,i)\<rbrakk> \<Longrightarrow> \<langle>a,b\<rangle> \<in> Vfrom(A,succ(succ(i)))"
-apply (unfold Pair_def)
+  unfolding Pair_def
 apply (blast intro: doubleton_in_Vfrom)
 done
 
@@ -249,13 +249,13 @@
 
 lemma Inl_in_VLimit:
     "\<lbrakk>a \<in> Vfrom(A,i); Limit(i)\<rbrakk> \<Longrightarrow> Inl(a) \<in> Vfrom(A,i)"
-apply (unfold Inl_def)
+  unfolding Inl_def
 apply (blast intro: zero_in_VLimit Pair_in_VLimit)
 done
 
 lemma Inr_in_VLimit:
     "\<lbrakk>b \<in> Vfrom(A,i); Limit(i)\<rbrakk> \<Longrightarrow> Inr(b) \<in> Vfrom(A,i)"
-apply (unfold Inr_def)
+  unfolding Inr_def
 apply (blast intro: one_in_VLimit Pair_in_VLimit)
 done
 
@@ -336,7 +336,7 @@
      \<Longrightarrow> a*b \<in> Vfrom(A, succ(succ(succ(j))))"
 apply (drule Transset_Vfrom)
 apply (rule subset_mem_Vfrom)
-apply (unfold Transset_def)
+  unfolding Transset_def
 apply (blast intro: Pair_in_Vfrom)
 done
 
@@ -352,10 +352,10 @@
 lemma sum_in_Vfrom:
     "\<lbrakk>a \<in> Vfrom(A,j);  b \<in> Vfrom(A,j);  Transset(A);  1:j\<rbrakk>
      \<Longrightarrow> a+b \<in> Vfrom(A, succ(succ(succ(j))))"
-apply (unfold sum_def)
+  unfolding sum_def
 apply (drule Transset_Vfrom)
 apply (rule subset_mem_Vfrom)
-apply (unfold Transset_def)
+  unfolding Transset_def
 apply (blast intro: zero_in_Vfrom Pair_in_Vfrom i_subset_Vfrom [THEN subsetD])
 done
 
@@ -371,7 +371,7 @@
 lemma fun_in_Vfrom:
     "\<lbrakk>a \<in> Vfrom(A,j);  b \<in> Vfrom(A,j);  Transset(A)\<rbrakk> \<Longrightarrow>
           a->b \<in> Vfrom(A, succ(succ(succ(succ(j)))))"
-apply (unfold Pi_def)
+  unfolding Pi_def
 apply (drule Transset_Vfrom)
 apply (rule subset_mem_Vfrom)
 apply (rule Collect_subset [THEN subset_trans])
@@ -380,7 +380,7 @@
 apply (rule_tac [3] Un_upper2)
 apply (rule_tac [2] succI1 [THEN UN_upper])
 apply (rule Pow_mono)
-apply (unfold Transset_def)
+  unfolding Transset_def
 apply (blast intro: Pair_in_Vfrom)
 done
 
@@ -395,7 +395,7 @@
     "\<lbrakk>a \<in> Vfrom(A,j);  Transset(A)\<rbrakk> \<Longrightarrow> Pow(a) \<in> Vfrom(A, succ(succ(j)))"
 apply (drule Transset_Vfrom)
 apply (rule subset_mem_Vfrom)
-apply (unfold Transset_def)
+  unfolding Transset_def
 apply (subst Vfrom, blast)
 done
 
@@ -476,12 +476,12 @@
 subsubsection\<open>Set Up an Environment for Simplification\<close>
 
 lemma rank_Inl: "rank(a) < rank(Inl(a))"
-apply (unfold Inl_def)
+  unfolding Inl_def
 apply (rule rank_pair2)
 done
 
 lemma rank_Inr: "rank(a) < rank(Inr(a))"
-apply (unfold Inr_def)
+  unfolding Inr_def
 apply (rule rank_pair2)
 done
 
@@ -491,7 +491,7 @@
 
 text\<open>NOT SUITABLE FOR REWRITING: recursive!\<close>
 lemma Vrec: "Vrec(a,H) = H(a, \<lambda>x\<in>Vset(rank(a)). Vrec(x,H))"
-apply (unfold Vrec_def)
+  unfolding Vrec_def
 apply (subst transrec, simp)
 apply (rule refl [THEN lam_cong, THEN subst_context], simp add: lt_def)
 done
@@ -507,7 +507,7 @@
 text\<open>NOT SUITABLE FOR REWRITING: recursive!\<close>
 lemma Vrecursor:
      "Vrecursor(H,a) = H(\<lambda>x\<in>Vset(rank(a)). Vrecursor(H,x),  a)"
-apply (unfold Vrecursor_def)
+  unfolding Vrecursor_def
 apply (subst transrec, simp)
 apply (rule refl [THEN lam_cong, THEN subst_context], simp add: lt_def)
 done
@@ -523,20 +523,20 @@
 subsection\<open>The Datatype Universe: \<^term>\<open>univ(A)\<close>\<close>
 
 lemma univ_mono: "A<=B \<Longrightarrow> univ(A) \<subseteq> univ(B)"
-apply (unfold univ_def)
+  unfolding univ_def
 apply (erule Vfrom_mono)
 apply (rule subset_refl)
 done
 
 lemma Transset_univ: "Transset(A) \<Longrightarrow> Transset(univ(A))"
-apply (unfold univ_def)
+  unfolding univ_def
 apply (erule Transset_Vfrom)
 done
 
 subsubsection\<open>The Set \<^term>\<open>univ(A)\<close> as a Limit\<close>
 
 lemma univ_eq_UN: "univ(A) = (\<Union>i\<in>nat. Vfrom(A,i))"
-apply (unfold univ_def)
+  unfolding univ_def
 apply (rule Limit_nat [THEN Limit_Vfrom_eq])
 done
 
@@ -567,7 +567,7 @@
 subsection\<open>Closure Properties for \<^term>\<open>univ(A)\<close>\<close>
 
 lemma zero_in_univ: "0 \<in> univ(A)"
-apply (unfold univ_def)
+  unfolding univ_def
 apply (rule nat_0I [THEN zero_in_Vfrom])
 done
 
@@ -575,7 +575,7 @@
 by (blast intro: zero_in_univ)
 
 lemma A_subset_univ: "A \<subseteq> univ(A)"
-apply (unfold univ_def)
+  unfolding univ_def
 apply (rule A_subset_Vfrom)
 done
 
@@ -584,30 +584,30 @@
 subsubsection\<open>Closure under Unordered and Ordered Pairs\<close>
 
 lemma singleton_in_univ: "a: univ(A) \<Longrightarrow> {a} \<in> univ(A)"
-apply (unfold univ_def)
+  unfolding univ_def
 apply (blast intro: singleton_in_VLimit Limit_nat)
 done
 
 lemma doubleton_in_univ:
     "\<lbrakk>a: univ(A);  b: univ(A)\<rbrakk> \<Longrightarrow> {a,b} \<in> univ(A)"
-apply (unfold univ_def)
+  unfolding univ_def
 apply (blast intro: doubleton_in_VLimit Limit_nat)
 done
 
 lemma Pair_in_univ:
     "\<lbrakk>a: univ(A);  b: univ(A)\<rbrakk> \<Longrightarrow> \<langle>a,b\<rangle> \<in> univ(A)"
-apply (unfold univ_def)
+  unfolding univ_def
 apply (blast intro: Pair_in_VLimit Limit_nat)
 done
 
 lemma Union_in_univ:
      "\<lbrakk>X: univ(A);  Transset(A)\<rbrakk> \<Longrightarrow> \<Union>(X) \<in> univ(A)"
-apply (unfold univ_def)
+  unfolding univ_def
 apply (blast intro: Union_in_VLimit Limit_nat)
 done
 
 lemma product_univ: "univ(A)*univ(A) \<subseteq> univ(A)"
-apply (unfold univ_def)
+  unfolding univ_def
 apply (rule Limit_nat [THEN product_VLimit])
 done
 
@@ -615,7 +615,7 @@
 subsubsection\<open>The Natural Numbers\<close>
 
 lemma nat_subset_univ: "nat \<subseteq> univ(A)"
-apply (unfold univ_def)
+  unfolding univ_def
 apply (rule i_subset_Vfrom)
 done
 
@@ -625,7 +625,7 @@
 subsubsection\<open>Instances for 1 and 2\<close>
 
 lemma one_in_univ: "1 \<in> univ(A)"
-apply (unfold univ_def)
+  unfolding univ_def
 apply (rule Limit_nat [THEN one_in_VLimit])
 done
 
@@ -634,7 +634,7 @@
 by (blast intro: nat_into_univ)
 
 lemma bool_subset_univ: "bool \<subseteq> univ(A)"
-apply (unfold bool_def)
+  unfolding bool_def
 apply (blast intro!: zero_in_univ one_in_univ)
 done
 
@@ -644,17 +644,17 @@
 subsubsection\<open>Closure under Disjoint Union\<close>
 
 lemma Inl_in_univ: "a: univ(A) \<Longrightarrow> Inl(a) \<in> univ(A)"
-apply (unfold univ_def)
+  unfolding univ_def
 apply (erule Inl_in_VLimit [OF _ Limit_nat])
 done
 
 lemma Inr_in_univ: "b: univ(A) \<Longrightarrow> Inr(b) \<in> univ(A)"
-apply (unfold univ_def)
+  unfolding univ_def
 apply (erule Inr_in_VLimit [OF _ Limit_nat])
 done
 
 lemma sum_univ: "univ(C)+univ(C) \<subseteq> univ(C)"
-apply (unfold univ_def)
+  unfolding univ_def
 apply (rule Limit_nat [THEN sum_VLimit])
 done
 
@@ -694,7 +694,7 @@
 lemmas Fin_subset_VLimit = subset_trans [OF Fin_mono Fin_VLimit]
 
 lemma Fin_univ: "Fin(univ(A)) \<subseteq> univ(A)"
-apply (unfold univ_def)
+  unfolding univ_def
 apply (rule Limit_nat [THEN Fin_VLimit])
 done
 
@@ -710,7 +710,7 @@
 lemmas nat_fun_subset_VLimit = subset_trans [OF Pi_mono nat_fun_VLimit]
 
 lemma nat_fun_univ: "n: nat \<Longrightarrow> n -> univ(A) \<subseteq> univ(A)"
-apply (unfold univ_def)
+  unfolding univ_def
 apply (erule nat_fun_VLimit [OF _ Limit_nat])
 done
 
@@ -726,7 +726,7 @@
 done
 
 lemma FiniteFun_univ1: "univ(A) -||> univ(A) \<subseteq> univ(A)"
-apply (unfold univ_def)
+  unfolding univ_def
 apply (rule Limit_nat [THEN FiniteFun_VLimit1])
 done
 
@@ -740,7 +740,7 @@
 
 lemma FiniteFun_univ:
     "W \<subseteq> univ(A) \<Longrightarrow> W -||> univ(A) \<subseteq> univ(A)"
-apply (unfold univ_def)
+  unfolding univ_def
 apply (erule FiniteFun_VLimit [OF _ Limit_nat])
 done
 
@@ -777,7 +777,7 @@
 lemma Pair_in_Vfrom_D:
     "\<lbrakk>\<langle>a,b\<rangle> \<in> Vfrom(X,succ(i));  Transset(X)\<rbrakk>
      \<Longrightarrow> a \<in> Vfrom(X,i)  \<and>  b \<in> Vfrom(X,i)"
-apply (unfold Pair_def)
+  unfolding Pair_def
 apply (blast dest!: doubleton_in_Vfrom_D Vfrom_doubleton_D)
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/WF.thy
--- a/src/ZF/WF.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/WF.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -109,7 +109,7 @@
     "\<lbrakk>wf(r);
         \<And>x.\<lbrakk>\<forall>y. \<langle>y,x\<rangle>: r \<longrightarrow> P(y)\<rbrakk> \<Longrightarrow> P(x)\<rbrakk>
      \<Longrightarrow> P(a)"
-apply (unfold wf_def)
+  unfolding wf_def
 apply (erule_tac x = "{z \<in> domain(r). \<not> P(z)}" in allE)
 apply blast
 done
@@ -132,7 +132,7 @@
     "\<lbrakk>wf[A](r);  a \<in> A;
         \<And>x.\<lbrakk>x \<in> A;  \<forall>y\<in>A. \<langle>y,x\<rangle>: r \<longrightarrow> P(y)\<rbrakk> \<Longrightarrow> P(x)
 \<rbrakk>  \<Longrightarrow>  P(a)"
-apply (unfold wf_on_def)
+  unfolding wf_on_def
 apply (erule wf_induct2, assumption)
 apply (rule field_Int_square, blast)
 done
@@ -220,7 +220,7 @@
 subsection\<open>The Predicate \<^term>\<open>is_recfun\<close>\<close>
 
 lemma is_recfun_type: "is_recfun(r,a,H,f) \<Longrightarrow> f \<in> r-``{a} -> range(f)"
-apply (unfold is_recfun_def)
+  unfolding is_recfun_def
 apply (erule ssubst)
 apply (rule lamI [THEN rangeI, THEN lam_type], assumption)
 done
@@ -229,7 +229,7 @@
 
 lemma apply_recfun:
     "\<lbrakk>is_recfun(r,a,H,f); \<langle>x,a\<rangle>:r\<rbrakk> \<Longrightarrow> f`x = H(x, restrict(f,r-``{x}))"
-apply (unfold is_recfun_def)
+  unfolding is_recfun_def
   txt\<open>replace f only on the left-hand side\<close>
 apply (erule_tac P = "\<lambda>x. t(x) = u" for t u in ssubst)
 apply (simp add: underI)
@@ -271,7 +271,7 @@
 
 lemma the_recfun_eq:
     "\<lbrakk>is_recfun(r,a,H,f);  wf(r);  trans(r)\<rbrakk> \<Longrightarrow> the_recfun(r,a,H) = f"
-apply (unfold the_recfun_def)
+  unfolding the_recfun_def
 apply (blast intro: is_recfun_functional)
 done
 
@@ -319,7 +319,7 @@
 lemma wftrec:
     "\<lbrakk>wf(r);  trans(r)\<rbrakk> \<Longrightarrow>
           wftrec(r,a,H) = H(a, \<lambda>x\<in>r-``{a}. wftrec(r,x,H))"
-apply (unfold wftrec_def)
+  unfolding wftrec_def
 apply (subst unfold_the_recfun [unfolded is_recfun_def])
 apply (simp_all add: vimage_singleton_iff [THEN iff_sym] the_recfun_cut)
 done
@@ -330,7 +330,7 @@
 (*NOT SUITABLE FOR REWRITING: it is recursive!*)
 lemma wfrec:
     "wf(r) \<Longrightarrow> wfrec(r,a,H) = H(a, \<lambda>x\<in>r-``{a}. wfrec(r,x,H))"
-apply (unfold wfrec_def)
+  unfolding wfrec_def
 apply (erule wf_trancl [THEN wftrec, THEN ssubst])
  apply (rule trans_trancl)
 apply (rule vimage_pair_mono [THEN restrict_lam_eq, THEN subst_context])
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/ZF_Base.thy
--- a/src/ZF/ZF_Base.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/ZF_Base.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -365,7 +365,7 @@
 
 (*Rule in Modus Ponens style [was called subsetE] *)
 lemma subsetD [elim]: "\<lbrakk>A \<subseteq> B;  c\<in>A\<rbrakk> \<Longrightarrow> c\<in>B"
-apply (unfold subset_def)
+  unfolding subset_def
 apply (erule bspec, assumption)
 done
 
@@ -430,7 +430,7 @@
 
 lemma Replace_iff:
     "b \<in> {y. x\<in>A, P(x,y)}  <->  (\<exists>x\<in>A. P(x,b) \<and> (\<forall>y. P(x,y) \<longrightarrow> y=b))"
-apply (unfold Replace_def)
+  unfolding Replace_def
 apply (rule replacement [THEN iff_trans], blast+)
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/Zorn.thy
--- a/src/ZF/Zorn.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/Zorn.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -70,7 +70,7 @@
 subsection\<open>The Transfinite Construction\<close>
 
 lemma increasingD1: "f \<in> increasing(A) \<Longrightarrow> f \<in> Pow(A)->Pow(A)"
-apply (unfold increasing_def)
+  unfolding increasing_def
 apply (erule CollectD1)
 done
 
@@ -182,17 +182,17 @@
 text\<open>* Defining the "next" operation for Hausdorff's Theorem *\<close>
 
 lemma chain_subset_Pow: "chain(A) \<subseteq> Pow(A)"
-apply (unfold chain_def)
+  unfolding chain_def
 apply (rule Collect_subset)
 done
 
 lemma super_subset_chain: "super(A,c) \<subseteq> chain(A)"
-apply (unfold super_def)
+  unfolding super_def
 apply (rule Collect_subset)
 done
 
 lemma maxchain_subset_chain: "maxchain(A) \<subseteq> chain(A)"
-apply (unfold maxchain_def)
+  unfolding maxchain_def
 apply (rule Collect_subset)
 done
 
@@ -220,7 +220,7 @@
                    if X \<in> chain(S) - maxchain(S) then ch ` super(S, X) else X"
        in bexI)
 apply force
-apply (unfold increasing_def)
+  unfolding increasing_def
 apply (rule CollectI)
 apply (rule lam_type)
 apply (simp (no_asm_simp))
@@ -245,7 +245,7 @@
 apply (erule TFin_induct)
 apply (simp (no_asm_simp) add: chain_subset_Pow [THEN subsetD, THEN PowD]
             choice_super [THEN super_subset_chain [THEN subsetD]])
-apply (unfold chain_def)
+  unfolding chain_def
 apply (rule CollectI, blast, safe)
 apply (rule_tac m1=B and n1=Ba in TFin_subset_linear [THEN disjE], fast+)
       txt\<open>\<open>Blast_tac's\<close> slow\<close>
@@ -377,7 +377,7 @@
 apply (rule_tac x="\<lambda>X\<in>Pow(S). if X=S then S else cons(ch`(S-X), X)"
        in bexI)
 apply force
-apply (unfold increasing_def)
+  unfolding increasing_def
 apply (rule CollectI)
 apply (rule lam_type)
 txt\<open>Type checking is surprisingly hard!\<close>
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/equalities.thy
--- a/src/ZF/equalities.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/equalities.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -621,7 +621,7 @@
 (** Range **)
 
 lemma rangeI [intro]: "\<langle>a,b\<rangle>\<in> r \<Longrightarrow> b \<in> range(r)"
-apply (unfold range_def)
+  unfolding range_def
 apply (erule converseI [THEN domainI])
 done
 
@@ -629,7 +629,7 @@
 by (unfold range_def, blast)
 
 lemma range_subset: "range(A*B) \<subseteq> B"
-apply (unfold range_def)
+  unfolding range_def
 apply (subst converse_prod)
 apply (rule domain_subset)
 done
@@ -682,12 +682,12 @@
 by blast
 
 lemma domain_subset_field: "domain(r) \<subseteq> field(r)"
-apply (unfold field_def)
+  unfolding field_def
 apply (rule Un_upper1)
 done
 
 lemma range_subset_field: "range(r) \<subseteq> field(r)"
-apply (unfold field_def)
+  unfolding field_def
 apply (rule Un_upper2)
 done
 
@@ -807,7 +807,7 @@
 done
 
 lemma vimage_subset: "r \<subseteq> A*B \<Longrightarrow> r-``C \<subseteq> A"
-apply (unfold vimage_def)
+  unfolding vimage_def
 apply (erule converse_type [THEN image_subset])
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/ex/Commutation.thy
--- a/src/ZF/ex/Commutation.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/ex/Commutation.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -63,7 +63,7 @@
 
 lemma commute_rtrancl:
   "commute(r,s) \<Longrightarrow> field(r)=field(s) \<Longrightarrow> commute(r^*,s^*)"
-apply (unfold commute_def)
+  unfolding commute_def
 apply (rule square_rtrancl)
 apply (rule square_sym [THEN square_rtrancl, THEN square_sym])
 apply (simp_all add: rtrancl_field)
@@ -95,7 +95,7 @@
 lemma confluent_Un:
  "\<lbrakk>confluent(r); confluent(s); commute(r^*, s^*);
      relation(r); relation(s)\<rbrakk> \<Longrightarrow> confluent(r \<union> s)"
-apply (unfold confluent_def)
+  unfolding confluent_def
 apply (rule rtrancl_Un_rtrancl [THEN subst], auto)
 apply (blast dest: diamond_Un intro: diamond_confluent [THEN confluentD])
 done
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/ex/Limit.thy
--- a/src/ZF/ex/Limit.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/ex/Limit.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -470,7 +470,7 @@
 
 lemma matrix_chain_left:
     "\<lbrakk>matrix(D,M); n \<in> nat\<rbrakk> \<Longrightarrow> chain(D,M`n)"
-apply (unfold chain_def)
+  unfolding chain_def
 apply (auto intro: matrix_fun [THEN apply_type] matrix_in matrix_rel_0_1)
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/ex/Ramsey.thy
--- a/src/ZF/ex/Ramsey.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/ex/Ramsey.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -69,7 +69,7 @@
 
 lemma Atleast_succD: 
     "Atleast(succ(m),A) \<Longrightarrow> \<exists>x \<in> A. Atleast(m, A-{x})"
-apply (unfold Atleast_def)
+  unfolding Atleast_def
 apply (blast dest: inj_is_fun [THEN apply_type] inj_succ_restrict)
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/func.thy
--- a/src/ZF/func.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/func.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -64,7 +64,7 @@
 by (unfold apply_def function_def, blast)
 
 lemma apply_equality: "\<lbrakk>\<langle>a,b\<rangle>: f;  f \<in> Pi(A,B)\<rbrakk> \<Longrightarrow> f`a = b"
-apply (unfold Pi_def)
+  unfolding Pi_def
 apply (blast intro: function_apply_equality)
 done
 
@@ -132,7 +132,7 @@
 subsection\<open>Lambda Abstraction\<close>
 
 lemma lamI: "a \<in> A \<Longrightarrow> <a,b(a)> \<in> (\<lambda>x\<in>A. b(x))"
-apply (unfold lam_def)
+  unfolding lam_def
 apply (erule RepFunI)
 done
 
@@ -304,7 +304,7 @@
 by (unfold restrict_def, blast)
 
 lemma domain_restrict [simp]: "domain(restrict(f,C)) = domain(f) \<inter> C"
-apply (unfold restrict_def)
+  unfolding restrict_def
 apply (auto simp add: domain_def)
 done
 
@@ -352,7 +352,7 @@
     "\<lbrakk>\<forall>f\<in>S. \<exists>C D. f \<in> C->D;
              \<forall>f\<in>S. \<forall>y\<in>S. f<=y | y<=f\<rbrakk> \<Longrightarrow>
           \<Union>(S) \<in> domain(\<Union>(S)) -> range(\<Union>(S))"
-apply (unfold Pi_def)
+  unfolding Pi_def
 apply (blast intro!: rel_Union function_Union)
 done
 
@@ -468,7 +468,7 @@
 done
 
 lemma update_idem: "\<lbrakk>f`x = y;  f \<in> Pi(A,B);  x \<in> A\<rbrakk> \<Longrightarrow> f(x:=y) = f"
-apply (unfold update_def)
+  unfolding update_def
 apply (simp add: domain_of_fun cons_absorb)
 apply (rule fun_extension)
 apply (best intro: apply_type if_type lam_type, assumption, simp)
@@ -482,7 +482,7 @@
 by (unfold update_def, simp)
 
 lemma update_type: "\<lbrakk>f \<in> Pi(A,B);  x \<in> A;  y \<in> B(x)\<rbrakk> \<Longrightarrow> f(x:=y) \<in> Pi(A, B)"
-apply (unfold update_def)
+  unfolding update_def
 apply (simp add: domain_of_fun cons_absorb apply_funtype lam_type)
 done
 
@@ -539,7 +539,7 @@
 by (blast intro: lam_type elim: Pi_lamE)
 
 lemma lam_mono: "A<=B \<Longrightarrow> Lambda(A,c) \<subseteq> Lambda(B,c)"
-apply (unfold lam_def)
+  unfolding lam_def
 apply (erule RepFun_mono)
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/pair.thy
--- a/src/ZF/pair.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/pair.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -46,7 +46,7 @@
 lemmas Pair_inject2 = Pair_iff [THEN iffD1, THEN conjunct2]
 
 lemma Pair_not_0: "\<langle>a,b\<rangle> \<noteq> 0"
-apply (unfold Pair_def)
+  unfolding Pair_def
 apply (blast elim: equalityE)
 done
 
diff -r a642599ffdea -r 9fc34f76b4e8 src/ZF/upair.thy
--- a/src/ZF/upair.thy	Tue Sep 27 17:46:52 2022 +0100
+++ b/src/ZF/upair.thy	Tue Sep 27 17:54:20 2022 +0100
@@ -66,7 +66,7 @@
 subsection\<open>Rules for Binary Intersection, Defined via \<^term>\<open>Upair\<close>\<close>
 
 lemma Int_iff [simp]: "c \<in> A \<inter> B \<longleftrightarrow> (c \<in> A \<and> c \<in> B)"
-apply (unfold Int_def)
+  unfolding Int_def
 apply (blast intro: UpairI1 UpairI2 elim: UpairE)
 done
 
@@ -104,7 +104,7 @@
 subsection\<open>Rules for \<^term>\<open>cons\<close>\<close>
 
 lemma cons_iff [simp]: "a \<in> cons(b,A) \<longleftrightarrow> (a=b | a \<in> A)"
-apply (unfold cons_def)
+  unfolding cons_def
 apply (blast intro: UpairI1 UpairI2 elim: UpairE)
 done
 
@@ -152,7 +152,7 @@
 
 lemma the_equality [intro]:
     "\<lbrakk>P(a);  \<And>x. P(x) \<Longrightarrow> x=a\<rbrakk> \<Longrightarrow> (THE x. P(x)) = a"
-apply (unfold the_def)
+  unfolding the_def
 apply (fast dest: subst)
 done
 
@@ -171,7 +171,7 @@
 
 (*If it's "undefined", it's zero!*)
 lemma the_0: "\<not> (\<exists>!x. P(x)) \<Longrightarrow> (THE x. P(x))=0"
-apply (unfold the_def)
+  unfolding the_def
 apply (blast elim!: ReplaceE)
 done