# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1664298154 -3600
# Node ID 8655344f1cf664ba0ab83cbde6fa8fe1f26d0ef0
# Parent  9fc34f76b4e85939fe6c910790aaadde2f3a828c
More obsolete "unfold" calls

diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/AC/AC15_WO6.thy
--- a/src/ZF/AC/AC15_WO6.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/AC/AC15_WO6.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -134,7 +134,7 @@
 (* ********************************************************************** *)
 
 theorem AC12_AC15: "AC12 \<Longrightarrow> AC15"
-apply (unfold AC12_def AC15_def)
+  unfolding AC12_def AC15_def
 apply (blast del: ballI 
              intro!: cons_times_nat_not_Finite ex_fun_AC13_AC15)
 done
@@ -168,7 +168,7 @@
 done
 
 theorem AC15_WO6: "AC15 \<Longrightarrow> WO6"
-apply (unfold AC15_def WO6_def)
+  unfolding AC15_def WO6_def
 apply (rule allI)
 apply (erule_tac x = "Pow (A) -{0}" in allE)
 apply (erule impE, fast)
@@ -212,7 +212,7 @@
 (* ********************************************************************** *)
 
 lemma AC1_AC13: "AC1 \<Longrightarrow> AC13(1)"
-apply (unfold AC1_def AC13_def)
+  unfolding AC1_def AC13_def
 apply (rule allI)
 apply (erule allE)
 apply (rule impI)
@@ -272,7 +272,7 @@
 done
 
 theorem AC13_AC1: "AC13(1) \<Longrightarrow> AC1"
-apply (unfold AC13_def AC1_def)
+  unfolding AC13_def AC1_def
 apply (fast elim!: AC13_AC1_lemma)
 done
 
@@ -281,7 +281,7 @@
 (* ********************************************************************** *)
 
 theorem AC11_AC14: "AC11 \<Longrightarrow> AC14"
-apply (unfold AC11_def AC14_def)
+  unfolding AC11_def AC14_def
 apply (fast intro!: AC10_AC13)
 done
 
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/AC/AC16_WO4.thy
--- a/src/ZF/AC/AC16_WO4.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/AC/AC16_WO4.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -87,7 +87,7 @@
 done
 
 lemma succ_not_lepoll_imp_eqpoll: "\<lbrakk>\<not>A \<approx> B; A \<lesssim> B\<rbrakk> \<Longrightarrow> succ(A) \<lesssim> B"
-apply (unfold lepoll_def eqpoll_def bij_def surj_def)
+  unfolding lepoll_def eqpoll_def bij_def surj_def
 apply (fast elim!: succ_not_lepoll_lemma inj_is_fun)
 done
 
@@ -254,7 +254,7 @@
 lemma sI: 
       "\<lbrakk>w \<in> t_n; cons(b,cons(u,a)) \<subseteq> w; a \<subseteq> y; b \<in> y-a; l \<approx> a\<rbrakk> 
        \<Longrightarrow> w \<in> s(u)"
-apply (unfold s_def succ_def k_def)
+  unfolding s_def succ_def k_def
 apply (blast intro!: eqpoll_imp_lepoll [THEN cons_lepoll_cong]
              intro: subset_imp_lepoll lepoll_trans)
 done
@@ -394,7 +394,7 @@
 
 
 lemma LL_subset: "LL \<subseteq> {z \<in> Pow(y). z \<lesssim> succ(k #+ m)}"
-apply (unfold LL_def MM_def)
+  unfolding LL_def MM_def
 apply (insert "includes")
 apply (blast intro: subset_imp_lepoll eqpoll_imp_lepoll lepoll_trans)
 done
@@ -563,7 +563,7 @@
 
 theorem AC16_WO4: 
      "\<lbrakk>AC_Equiv.AC16(k #+ m, k); 0 < k; 0 < m; k \<in> nat; m \<in> nat\<rbrakk> \<Longrightarrow> WO4(m)"
-apply (unfold AC_Equiv.AC16_def WO4_def)
+  unfolding AC_Equiv.AC16_def WO4_def
 apply (rule allI)
 apply (case_tac "Finite (A)")
 apply (rule lemma1, assumption+)
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/AC/AC16_lemmas.thy
--- a/src/ZF/AC/AC16_lemmas.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/AC/AC16_lemmas.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -46,7 +46,7 @@
 done
 
 lemma eqpoll_RepFun_sing: "X\<approx>{{x}. x \<in> X}"
-apply (unfold eqpoll_def bij_def)
+  unfolding eqpoll_def bij_def
 apply (rule_tac x = "\<lambda>x \<in> X. {x}" in exI)
 apply (rule IntI)
 apply (unfold inj_def surj_def, simp)
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/AC/AC17_AC1.thy
--- a/src/ZF/AC/AC17_AC1.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/AC/AC17_AC1.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -19,7 +19,7 @@
 by (fast intro!: lam_type apply_type)
 
 lemma AC0_AC1: "AC0 \<Longrightarrow> AC1"
-apply (unfold AC0_def AC1_def)
+  unfolding AC0_def AC1_def
 apply (blast intro: AC0_AC1_lemma)
 done
 
@@ -35,7 +35,7 @@
 done
 
 lemma AC1_AC17: "AC1 \<Longrightarrow> AC17"
-apply (unfold AC1_def AC17_def)
+  unfolding AC1_def AC17_def
 apply (rule allI)
 apply (rule ballI)
 apply (erule_tac x = "Pow (A) -{0}" in allE)
@@ -152,7 +152,7 @@
 by (unfold pairwise_disjoint_def, fast)
 
 lemma AC1_AC2: "AC1 \<Longrightarrow> AC2"
-apply (unfold AC1_def AC2_def)
+  unfolding AC1_def AC2_def
 apply (rule allI)
 apply (rule impI)  
 apply (elim asm_rl conjE allE exE impE, assumption)
@@ -185,7 +185,7 @@
 done
 
 lemma AC2_AC1: "AC2 \<Longrightarrow> AC1"
-apply (unfold AC1_def AC2_def pairwise_disjoint_def)
+  unfolding AC1_def AC2_def pairwise_disjoint_def
 apply (intro allI impI)
 apply (elim allE impE)
 prefer 2 apply (fast elim!: AC2_AC1_aux3) 
@@ -201,7 +201,7 @@
 by blast
 
 lemma AC1_AC4: "AC1 \<Longrightarrow> AC4"
-apply (unfold AC1_def AC4_def)
+  unfolding AC1_def AC4_def
 apply (intro allI impI)
 apply (drule spec, drule mp [OF _ empty_notin_images]) 
 apply (best intro!: lam_type elim!: apply_type)
@@ -222,7 +222,7 @@
 by fast
 
 lemma AC4_AC3: "AC4 \<Longrightarrow> AC3"
-apply (unfold AC3_def AC4_def)
+  unfolding AC3_def AC4_def
 apply (intro allI ballI)
 apply (elim allE impE)
 apply (erule AC4_AC3_aux1)
@@ -240,7 +240,7 @@
 done
 
 lemma AC3_AC1: "AC3 \<Longrightarrow> AC1"
-apply (unfold AC1_def AC3_def)
+  unfolding AC1_def AC3_def
 apply (fast intro!: id_type elim: AC3_AC1_lemma [THEN subst])
 done
 
@@ -249,7 +249,7 @@
 (* ********************************************************************** *)
 
 lemma AC4_AC5: "AC4 \<Longrightarrow> AC5"
-apply (unfold range_def AC4_def AC5_def)
+  unfolding range_def AC4_def AC5_def
 apply (intro allI ballI)
 apply (elim allE impE)
 apply (erule fun_is_rel [THEN converse_type])
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/AC/AC7_AC9.thy
--- a/src/ZF/AC/AC7_AC9.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/AC/AC7_AC9.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -69,7 +69,7 @@
 by (blast dest: Sigma_fun_space_not0)
 
 lemma AC7_AC6: "AC7 \<Longrightarrow> AC6"
-apply (unfold AC6_def AC7_def)
+  unfolding AC6_def AC7_def
 apply (rule allI)
 apply (rule impI)
 apply (case_tac "A=0", simp)
@@ -97,7 +97,7 @@
 done
 
 lemma AC1_AC8: "AC1 \<Longrightarrow> AC8"
-apply (unfold AC1_def AC8_def)
+  unfolding AC1_def AC8_def
 apply (fast dest: AC1_AC8_lemma1 AC1_AC8_lemma2)
 done
 
@@ -114,7 +114,7 @@
 by fast
 
 lemma AC8_AC9: "AC8 \<Longrightarrow> AC9"
-apply (unfold AC8_def AC9_def)
+  unfolding AC8_def AC9_def
 apply (intro allI impI)
 apply (erule allE)
 apply (erule impE, erule AC8_AC9_lemma, force) 
@@ -159,7 +159,7 @@
 done
 
 lemma AC9_AC1: "AC9 \<Longrightarrow> AC1"
-apply (unfold AC1_def AC9_def)
+  unfolding AC1_def AC9_def
 apply (intro allI impI)
 apply (erule allE)
 apply (case_tac "A\<noteq>0")
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/AC/DC.thy
--- a/src/ZF/AC/DC.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/AC/DC.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -136,7 +136,7 @@
 by (unfold RR_def, fast)
 
 lemma lemma1_2: "RR \<noteq> 0"
-apply (unfold RR_def XX_def)
+  unfolding RR_def XX_def
 apply (rule all_ex [THEN ballE])
 apply (erule_tac [2] notE [OF _ empty_subsetI [THEN PowI]])
 apply (erule_tac impE [OF _ nat_0I [THEN n_lesspoll_nat]])
@@ -153,7 +153,7 @@
 done
 
 lemma lemma1_3: "range(RR) \<subseteq> domain(RR)"
-apply (unfold RR_def XX_def)
+  unfolding RR_def XX_def
 apply (rule range_subset_domain, blast, clarify)
 apply (frule fun_is_rel [THEN image_subset, THEN PowI, 
                          THEN all_ex [THEN bspec]])
@@ -326,7 +326,7 @@
              succ(\<Union>f \<in> Y. domain(f)) \<and> (\<forall>f\<in>Y. restrict(g, domain(f)) = f)")
 apply (simp add: RR_def, blast)
 apply (safe del: domainE)
-apply (unfold XX_def RR_def)
+  unfolding XX_def RR_def
 apply (rule rev_bexI, erule singleton_in_funs)
 apply (simp add: nat_0I [THEN rev_bexI] cons_fun_type2)
 done
@@ -393,7 +393,7 @@
      "\<lbrakk>\<forall>b<nat. <f``b, f`b> \<in> RR;   
          f \<in> nat -> XX; range(R) \<subseteq> domain(R); x \<in> domain(R)\<rbrakk>    
       \<Longrightarrow> allRR"
-apply (unfold RR_def allRR_def)
+  unfolding RR_def allRR_def
 apply (rule oallI, drule ltD)
 apply (erule nat_induct)
 apply (drule_tac x=0 in ospec, blast intro: Limit_has_0) 
@@ -463,7 +463,7 @@
 
 
 theorem DC_nat_imp_DC0: "DC(nat) \<Longrightarrow> DC0"
-apply (unfold DC_def DC0_def)
+  unfolding DC_def DC0_def
 apply (intro allI impI)
 apply (erule asm_rl conjE ex_in_domain [THEN exE] allE)+
 apply (erule impE [OF _ imp_DC0.lemma4], assumption+)
@@ -504,7 +504,7 @@
 done
 
 theorem DC_WO3: "(\<forall>K. Card(K) \<longrightarrow> DC(K)) \<Longrightarrow> WO3"
-apply (unfold DC_def WO3_def)
+  unfolding DC_def WO3_def
 apply (rule allI)
 apply (case_tac "A \<prec> Hartog (A)")
 apply (fast dest!: lesspoll_imp_ex_lt_eqpoll 
@@ -572,7 +572,7 @@
 done
 
 theorem WO1_DC_Card: "WO1 \<Longrightarrow> \<forall>K. Card(K) \<longrightarrow> DC(K)"
-apply (unfold DC_def WO1_def)
+  unfolding DC_def WO1_def
 apply (rule allI impI)+
 apply (erule allE exE conjE)+
 apply (rule_tac x = "\<lambda>b \<in> K. ff (b, X, Ra, R) " in bexI)
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/AC/HH.thy
--- a/src/ZF/AC/HH.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/AC/HH.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -99,7 +99,7 @@
 
 lemma HH_subset_x_imp_lepoll: 
      "\<lbrakk>HH(f, x, i) \<in> Pow(x)-{0}; Ord(i)\<rbrakk> \<Longrightarrow> i \<lesssim> Pow(x)-{0}"
-apply (unfold lepoll_def inj_def)
+  unfolding lepoll_def inj_def
 apply (rule_tac x = "\<lambda>j \<in> i. HH (f, x, j) " in exI)
 apply (simp (no_asm_simp))
 apply (fast del: DiffE
@@ -235,7 +235,7 @@
 done
 
 lemma AC1_WO2: "AC1 \<Longrightarrow> WO2"
-apply (unfold AC1_def WO2_def eqpoll_def)
+  unfolding AC1_def WO2_def eqpoll_def
 apply (intro allI) 
 apply (drule_tac x = "Pow(A) - {0}" in spec) 
 apply (blast dest: bijection)
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/AC/WO1_AC.thy
--- a/src/ZF/AC/WO1_AC.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/AC/WO1_AC.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -83,7 +83,7 @@
 
 lemma lemma2_5: 
      "f \<in> bij(D+D, B) \<Longrightarrow> \<Union>({{f`Inl(i), f`Inr(i)}. i \<in> D})=B"
-apply (unfold bij_def surj_def)
+  unfolding bij_def surj_def
 apply (fast elim!: inj_is_fun [THEN apply_type])
 done
 
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/AC/WO1_WO7.thy
--- a/src/ZF/AC/WO1_WO7.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/AC/WO1_WO7.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -21,7 +21,7 @@
 (* ********************************************************************** *)
 
 lemma WO7_iff_LEMMA: "WO7 \<longleftrightarrow> LEMMA"
-apply (unfold WO7_def LEMMA_def)
+  unfolding WO7_def LEMMA_def
 apply (blast intro: Finite_well_ord_converse)
 done
 
@@ -30,7 +30,7 @@
 (* ********************************************************************** *)
 
 lemma LEMMA_imp_WO1: "LEMMA \<Longrightarrow> WO1"
-apply (unfold WO1_def LEMMA_def Finite_def eqpoll_def)
+  unfolding WO1_def LEMMA_def Finite_def eqpoll_def
 apply (blast intro!: well_ord_rvimage [OF bij_is_inj nat_implies_well_ord])
 done
 
@@ -49,7 +49,7 @@
 
 lemma converse_Memrel_not_wf_on: 
     "\<lbrakk>Ord(a); \<not>Finite(a)\<rbrakk> \<Longrightarrow> \<not>wf[a](converse(Memrel(a)))"
-apply (unfold wf_on_def wf_def)
+  unfolding wf_on_def wf_def
 apply (drule nat_le_infinite_Ord [THEN le_imp_subset], assumption)
 apply (rule notI)
 apply (erule_tac x = nat in allE, blast)
@@ -102,7 +102,7 @@
 
 (* The implication "WO8 \<Longrightarrow> WO1": a faithful image of Rubin \<and> Rubin's proof*)
 lemma WO8_WO1: "WO8 \<Longrightarrow> WO1"
-apply (unfold WO1_def WO8_def)
+  unfolding WO1_def WO8_def
 apply (rule allI)
 apply (erule_tac x = "{{x}. x \<in> A}" in allE)
 apply (erule impE)
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/AC/WO2_AC16.thy
--- a/src/ZF/AC/WO2_AC16.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/AC/WO2_AC16.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -394,7 +394,7 @@
       \<Longrightarrow> b=y"
 apply (drule subset_imp_eq)
 apply (erule_tac [3] nat_succI)
-apply (unfold bij_def inj_def)
+  unfolding bij_def inj_def
 apply (blast intro: eqpoll_sym eqpoll_imp_lepoll
              dest:  ltD apply_type)+
 done
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/AC/WO6_WO1.thy
--- a/src/ZF/AC/WO6_WO1.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/AC/WO6_WO1.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -66,7 +66,7 @@
 (* ********************************************************************** *)
 
 lemma WO3_WO1: "WO3 \<Longrightarrow> WO1"
-apply (unfold eqpoll_def WO1_def WO3_def)
+  unfolding eqpoll_def WO1_def WO3_def
 apply (intro allI)
 apply (drule_tac x=A in spec) 
 apply (blast intro: bij_is_inj well_ord_rvimage 
@@ -76,7 +76,7 @@
 (* ********************************************************************** *)
 
 lemma WO1_WO2: "WO1 \<Longrightarrow> WO2"
-apply (unfold eqpoll_def WO1_def WO2_def)
+  unfolding eqpoll_def WO1_def WO2_def
 apply (blast intro!: Ord_ordertype ordermap_bij)
 done
 
@@ -94,7 +94,7 @@
 by (fast dest!: surj_imp_eq' intro!: ltI elim!: ltE)
 
 lemma WO1_WO4: "WO1 \<Longrightarrow> WO4(1)"
-apply (unfold WO1_def WO4_def)
+  unfolding WO1_def WO4_def
 apply (rule allI)
 apply (erule_tac x = A in allE)
 apply (erule exE)
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/Bin.thy
--- a/src/ZF/Bin.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Bin.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -402,7 +402,7 @@
      "\<lbrakk>v \<in> bin;  w \<in> bin\<rbrakk>
       \<Longrightarrow> integ_of(v) $< integ_of(w)
           \<longleftrightarrow> znegative (integ_of (bin_add (v, bin_minus(w))))"
-apply (unfold zless_def zdiff_def)
+  unfolding zless_def zdiff_def
 apply (simp add: integ_of_minus integ_of_add)
 done
 
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/Cardinal.thy
--- a/src/ZF/Cardinal.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Cardinal.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -125,7 +125,7 @@
 
 (*Asymmetry law*)
 lemma eqpollI: "\<lbrakk>X \<lesssim> Y;  Y \<lesssim> X\<rbrakk> \<Longrightarrow> X \<approx> Y"
-apply (unfold lepoll_def eqpoll_def)
+  unfolding lepoll_def eqpoll_def
 apply (elim exE)
 apply (rule schroeder_bernstein, assumption+)
 done
@@ -138,7 +138,7 @@
 by (blast intro: eqpollI elim!: eqpollE)
 
 lemma lepoll_0_is_0: "A \<lesssim> 0 \<Longrightarrow> A = 0"
-apply (unfold lepoll_def inj_def)
+  unfolding lepoll_def inj_def
 apply (blast dest: apply_type)
 done
 
@@ -332,7 +332,7 @@
 (*Need AC to get @{term"X \<lesssim> Y \<Longrightarrow> |X| \<le> |Y|"};  see well_ord_lepoll_imp_cardinal_le
   Converse also requires AC, but see well_ord_cardinal_eqE*)
 lemma cardinal_cong: "X \<approx> Y \<Longrightarrow> |X| = |Y|"
-apply (unfold eqpoll_def cardinal_def)
+  unfolding eqpoll_def cardinal_def
 apply (rule Least_cong)
 apply (blast intro: comp_bij bij_converse_bij)
 done
@@ -380,13 +380,13 @@
 
 (* Could replace the  @{term"\<not>(j \<approx> i)"}  by  @{term"\<not>(i \<preceq> j)"}. *)
 lemma CardI: "\<lbrakk>Ord(i);  \<And>j. j<i \<Longrightarrow> \<not>(j \<approx> i)\<rbrakk> \<Longrightarrow> Card(i)"
-apply (unfold Card_def cardinal_def)
+  unfolding Card_def cardinal_def
 apply (subst Least_equality)
 apply (blast intro: eqpoll_refl)+
 done
 
 lemma Card_is_Ord: "Card(i) \<Longrightarrow> Ord(i)"
-apply (unfold Card_def cardinal_def)
+  unfolding Card_def cardinal_def
 apply (erule ssubst)
 apply (rule Ord_Least)
 done
@@ -621,7 +621,7 @@
 
 lemma nat_lepoll_imp_ex_eqpoll_n:
      "\<lbrakk>n \<in> nat;  nat \<lesssim> X\<rbrakk> \<Longrightarrow> \<exists>Y. Y \<subseteq> X \<and> n \<approx> Y"
-apply (unfold lepoll_def eqpoll_def)
+  unfolding lepoll_def eqpoll_def
 apply (fast del: subsetI subsetCE
             intro!: subset_SIs
             dest!: Ord_nat [THEN [2] OrdmemD, THEN [2] restrict_inj]
@@ -650,7 +650,7 @@
 
 lemma lesspoll_succ_imp_lepoll:
      "\<lbrakk>A \<prec> succ(m); m \<in> nat\<rbrakk> \<Longrightarrow> A \<lesssim> m"
-apply (unfold lesspoll_def lepoll_def eqpoll_def bij_def)
+  unfolding lesspoll_def lepoll_def eqpoll_def bij_def
 apply (auto dest: inj_not_surj_succ)
 done
 
@@ -951,7 +951,7 @@
 
 lemma Finite_imp_well_ord:
     "Finite(A) \<Longrightarrow> \<exists>r. well_ord(A,r)"
-apply (unfold Finite_def eqpoll_def)
+  unfolding Finite_def eqpoll_def
 apply (blast intro: well_ord_rvimage bij_is_inj well_ord_Memrel nat_into_Ord)
 done
 
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/CardinalArith.thy
--- a/src/ZF/CardinalArith.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/CardinalArith.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -293,14 +293,14 @@
 done
 
 lemma cmult_1 [simp]: "Card(K) \<Longrightarrow> 1 \<otimes> K = K"
-apply (unfold cmult_def succ_def)
+  unfolding cmult_def succ_def
 apply (simp add: prod_singleton_eqpoll [THEN cardinal_cong] Card_cardinal_eq)
 done
 
 subsection\<open>Some inequalities for multiplication\<close>
 
 lemma prod_square_lepoll: "A \<lesssim> A*A"
-apply (unfold lepoll_def inj_def)
+  unfolding lepoll_def inj_def
 apply (rule_tac x = "\<lambda>x\<in>A. \<langle>x,x\<rangle>" in exI, simp)
 done
 
@@ -317,7 +317,7 @@
 subsubsection\<open>Multiplication by a non-zero cardinal\<close>
 
 lemma prod_lepoll_self: "b \<in> B \<Longrightarrow> A \<lesssim> A*B"
-apply (unfold lepoll_def inj_def)
+  unfolding lepoll_def inj_def
 apply (rule_tac x = "\<lambda>x\<in>A. \<langle>x,b\<rangle>" in exI, simp)
 done
 
@@ -366,7 +366,7 @@
 (*Unconditional version requires AC*)
 lemma cmult_succ_lemma:
     "\<lbrakk>Ord(m);  Ord(n)\<rbrakk> \<Longrightarrow> succ(m) \<otimes> n = n \<oplus> (m \<otimes> n)"
-apply (unfold cmult_def cadd_def)
+  unfolding cmult_def cadd_def
 apply (rule prod_succ_eqpoll [THEN cardinal_cong, THEN trans])
 apply (rule cardinal_cong [symmetric])
 apply (rule sum_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll])
@@ -502,7 +502,7 @@
 
 lemma pred_csquare_subset:
     "z<K \<Longrightarrow> Order.pred(K*K, \<langle>z,z\<rangle>, csquare_rel(K)) \<subseteq> succ(z)*succ(z)"
-apply (unfold Order.pred_def)
+  unfolding Order.pred_def
 apply (safe del: SigmaI dest!: csquareD)
 apply (unfold lt_def, auto)
 done
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/Coind/ECR.thy
--- a/src/ZF/Coind/ECR.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Coind/ECR.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -61,7 +61,7 @@
 
 lemma basic_consistency_lem: 
   "\<lbrakk>ve \<in> ValEnv; te \<in> TyEnv; isofenv(ve,te)\<rbrakk> \<Longrightarrow> hastyenv(ve,te)"
-apply (unfold isofenv_def hastyenv_def)
+  unfolding isofenv_def hastyenv_def
 apply (force intro: te_appI ve_domI) 
 done
 
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/Coind/Map.thy
--- a/src/ZF/Coind/Map.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Coind/Map.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -81,7 +81,7 @@
 
 lemma mapQU:
   "\<lbrakk>m \<in> PMap(A,quniv(B)); \<And>x. x \<in> A \<Longrightarrow> x \<in> univ(B)\<rbrakk> \<Longrightarrow> m \<in> quniv(B)"
-apply (unfold PMap_def TMap_def)
+  unfolding PMap_def TMap_def
 apply (blast intro!: MapQU_lemma [THEN subsetD]) 
 done
 
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/Coind/Values.thy
--- a/src/ZF/Coind/Values.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Coind/Values.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -67,7 +67,7 @@
 
 
 lemma v_constNE [simp]: "c \<in> Const \<Longrightarrow> v_const(c) \<noteq> 0"
-apply (unfold QPair_def QInl_def QInr_def Val_ValEnv.con_defs)
+  unfolding QPair_def QInl_def QInr_def Val_ValEnv.con_defs
 apply (drule constNEE, auto)
 done
 
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/Constructible/L_axioms.thy
--- a/src/ZF/Constructible/L_axioms.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Constructible/L_axioms.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -205,7 +205,7 @@
 theorem Ex_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(z) \<and> P(x,z), \<lambda>a x. \<exists>z\<in>Lset(a). Q(a,x,z)]"
-apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def)
+  unfolding L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def
 apply (elim meta_exE)
 apply (rule meta_exI)
 apply (erule reflection.Ex_reflection [OF reflection_Lset])
@@ -214,7 +214,7 @@
 theorem All_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(z) \<longrightarrow> P(x,z), \<lambda>a x. \<forall>z\<in>Lset(a). Q(a,x,z)]"
-apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def)
+  unfolding L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def
 apply (elim meta_exE)
 apply (rule meta_exI)
 apply (erule reflection.All_reflection [OF reflection_Lset])
@@ -239,7 +239,7 @@
 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[##Lset(a)]. Q(a,x,z)]"
-apply (unfold setclass_def rex_def)
+  unfolding setclass_def rex_def
 apply (erule Rex_reflection [unfolded rex_def Bex_def]) 
 done
 
@@ -247,7 +247,7 @@
 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[##Lset(a)]. Q(a,x,z)]"
-apply (unfold setclass_def rall_def)
+  unfolding setclass_def rall_def
 apply (erule Rall_reflection [unfolded rall_def Ball_def]) 
 done
 
@@ -259,7 +259,7 @@
 lemma ReflectsD:
      "\<lbrakk>REFLECTS[P,Q]; Ord(i)\<rbrakk>
       \<Longrightarrow> \<exists>j. i<j \<and> (\<forall>x \<in> Lset(j). P(x) \<longleftrightarrow> Q(j,x))"
-apply (unfold L_Reflects_def Closed_Unbounded_def)
+  unfolding L_Reflects_def Closed_Unbounded_def
 apply (elim meta_exE, clarify)
 apply (blast dest!: UnboundedD)
 done
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/Constructible/Rank.thy
--- a/src/ZF/Constructible/Rank.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Constructible/Rank.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -39,7 +39,7 @@
 lemma  (in M_ordertype) wellordered_iso_subset_lemma: 
      "\<lbrakk>wellordered(M,A,r);  f \<in> ord_iso(A,r, A',r);  A'<= A;  y \<in> A;  
        M(A);  M(f);  M(r)\<rbrakk> \<Longrightarrow> \<not> <f`y, y> \<in> r"
-apply (unfold wellordered_def ord_iso_def)
+  unfolding wellordered_def ord_iso_def
 apply (elim conjE CollectE) 
 apply (erule wellfounded_on_induct, assumption+)
  apply (insert well_ord_iso_separation [of A f r])
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/Constructible/Reflection.thy
--- a/src/ZF/Constructible/Reflection.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Constructible/Reflection.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -187,7 +187,7 @@
      "\<lbrakk>y\<in>Mset(a); Cl(a); ClEx(P,a);
         \<And>a. \<lbrakk>Cl(a); Ord(a)\<rbrakk> \<Longrightarrow> \<forall>x\<in>Mset(a). P(x) \<longleftrightarrow> Q(a,x)\<rbrakk>
       \<Longrightarrow> (\<exists>z. M(z) \<and> P(\<langle>y,z\<rangle>)) \<longleftrightarrow> (\<exists>z\<in>Mset(a). Q(a,\<langle>y,z\<rangle>))"
-apply (unfold ClEx_def FF_def F0_def M_def)
+  unfolding ClEx_def FF_def F0_def M_def
 apply (rule ex_reflection.ZF_ClEx_iff
   [OF ex_reflection.intro, OF reflection.intro ex_reflection_axioms.intro,
     of Mset Cl])
@@ -204,7 +204,7 @@
 lemma Closed_Unbounded_ClEx:
      "(\<And>a. \<lbrakk>Cl(a); Ord(a)\<rbrakk> \<Longrightarrow> \<forall>x\<in>Mset(a). P(x) \<longleftrightarrow> Q(a,x))
       \<Longrightarrow> Closed_Unbounded(ClEx(P))"
-apply (unfold ClEx_eq FF_def F0_def M_def)
+  unfolding ClEx_eq FF_def F0_def M_def
 apply (rule ex_reflection.ZF_Closed_Unbounded_ClEx [of Mset _ _ Cl])
 apply (rule ex_reflection.intro, rule reflection_axioms)
 apply (blast intro: ex_reflection_axioms.intro)
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/Constructible/Relative.thy
--- a/src/ZF/Constructible/Relative.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Constructible/Relative.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -945,7 +945,7 @@
 
 lemma (in M_trivial) limit_ordinal_abs [simp]:
      "M(a) \<Longrightarrow> limit_ordinal(M,a) \<longleftrightarrow> Limit(a)"
-apply (unfold Limit_def limit_ordinal_def)
+  unfolding Limit_def limit_ordinal_def
 apply (simp add: Ord_0_lt_iff)
 apply (simp add: lt_def, blast)
 done
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/Constructible/Satisfies_absolute.thy
--- a/src/ZF/Constructible/Satisfies_absolute.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Constructible/Satisfies_absolute.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -890,7 +890,7 @@
        fun_apply(##Lset(i), rp, u, rpe) \<and> fun_apply(##Lset(i), rq, u, rqe) \<and>
        is_and(##Lset(i), rpe, rqe, andpq) \<and> is_not(##Lset(i), andpq, notpq) \<and>
        u \<in> list(A) \<and> pair(##Lset(i), u, notpq, x))]"
-apply (unfold is_and_def is_not_def) 
+  unfolding is_and_def is_not_def 
 apply (intro FOL_reflections function_reflections)
 done
 
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/Epsilon.thy
--- a/src/ZF/Epsilon.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Epsilon.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -48,7 +48,7 @@
 lemmas arg_into_eclose = arg_subset_eclose [THEN subsetD]
 
 lemma Transset_eclose: "Transset(eclose(A))"
-apply (unfold eclose_def Transset_def)
+  unfolding eclose_def Transset_def
 apply (rule subsetI [THEN ballI])
 apply (erule UN_E)
 apply (rule nat_succI [THEN UN_I], assumption)
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/EquivClass.thy
--- a/src/ZF/EquivClass.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/EquivClass.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -52,7 +52,7 @@
 (*second half*)
 lemma comp_equivI:
     "\<lbrakk>converse(r) O r = r;  domain(r) = A\<rbrakk> \<Longrightarrow> equiv(A,r)"
-apply (unfold equiv_def refl_def sym_def trans_def)
+  unfolding equiv_def refl_def sym_def trans_def
 apply (erule equalityE)
 apply (subgoal_tac "\<forall>x y. \<langle>x,y\<rangle> \<in> r \<longrightarrow> \<langle>y,x\<rangle> \<in> r", blast+)
 done
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/Finite.thy
--- a/src/ZF/Finite.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Finite.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -41,7 +41,7 @@
 subsection \<open>Finite Powerset Operator\<close>
 
 lemma Fin_mono: "A<=B \<Longrightarrow> Fin(A) \<subseteq> Fin(B)"
-apply (unfold Fin.defs)
+  unfolding Fin.defs
 apply (rule lfp_mono)
 apply (rule Fin.bnd_mono)+
 apply blast
@@ -130,7 +130,7 @@
 
 lemma FiniteFun_mono:
     "\<lbrakk>A<=C;  B<=D\<rbrakk> \<Longrightarrow> A -||> B  \<subseteq>  C -||> D"
-apply (unfold FiniteFun.defs)
+  unfolding FiniteFun.defs
 apply (rule lfp_mono)
 apply (rule FiniteFun.bnd_mono)+
 apply (intro Fin_mono Sigma_mono basic_monos, assumption+)
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/Induct/Binary_Trees.thy
--- a/src/ZF/Induct/Binary_Trees.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Induct/Binary_Trees.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -33,14 +33,14 @@
 \<close>
 
 lemma bt_mono: "A \<subseteq> B \<Longrightarrow> bt(A) \<subseteq> bt(B)"
-  apply (unfold bt.defs)
+    unfolding bt.defs
   apply (rule lfp_mono)
     apply (rule bt.bnd_mono)+
   apply (rule univ_mono basic_monos | assumption)+
   done
 
 lemma bt_univ: "bt(univ(A)) \<subseteq> univ(A)"
-  apply (unfold bt.defs bt.con_defs)
+    unfolding bt.defs bt.con_defs
   apply (rule lfp_lowerbound)
    apply (rule_tac [2] A_subset_univ [THEN univ_mono])
   apply (fast intro!: zero_in_univ Inl_in_univ Inr_in_univ Pair_in_univ)
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/Induct/Datatypes.thy
--- a/src/ZF/Induct/Datatypes.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Induct/Datatypes.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -32,14 +32,14 @@
 \<close>
 
 lemma data_mono: "\<lbrakk>A \<subseteq> C; B \<subseteq> D\<rbrakk> \<Longrightarrow> data(A, B) \<subseteq> data(C, D)"
-  apply (unfold data.defs)
+    unfolding data.defs
   apply (rule lfp_mono)
    apply (rule data.bnd_mono)+
   apply (rule univ_mono Un_mono basic_monos | assumption)+
   done
 
 lemma data_univ: "data(univ(A), univ(A)) \<subseteq> univ(A)"
-  apply (unfold data.defs data.con_defs)
+    unfolding data.defs data.con_defs
   apply (rule lfp_lowerbound)
    apply (rule_tac [2] subset_trans [OF A_subset_univ Un_upper1, THEN univ_mono])
   apply (fast intro!: zero_in_univ Inl_in_univ Inr_in_univ Pair_in_univ)
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/Induct/ListN.thy
--- a/src/ZF/Induct/ListN.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Induct/ListN.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -37,7 +37,7 @@
   done
 
 lemma listn_mono: "A \<subseteq> B \<Longrightarrow> listn(A) \<subseteq> listn(B)"
-  apply (unfold listn.defs)
+    unfolding listn.defs
   apply (rule lfp_mono)
     apply (rule listn.bnd_mono)+
   apply (assumption | rule univ_mono Sigma_mono list_mono basic_monos)+
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/Induct/Multiset.thy
--- a/src/ZF/Induct/Multiset.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Induct/Multiset.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -268,12 +268,12 @@
 by (auto intro!: lam_cong simp add: munion_def)
 
 lemma munion_assoc: "(M +# N) +# K = M +# (N +# K)"
-apply (unfold munion_def mset_of_def)
+  unfolding munion_def mset_of_def
 apply (rule lam_cong, auto)
 done
 
 lemma munion_lcommute: "M +# (N +# K) = N +# (M +# K)"
-apply (unfold munion_def mset_of_def)
+  unfolding munion_def mset_of_def
 apply (rule lam_cong, auto)
 done
 
@@ -291,7 +291,7 @@
 by (auto simp add: multiset_def mdiff_def normalize_def multiset_fun_iff mset_of_def funrestrict_def)
 
 lemma mdiff_union_inverse2 [simp]: "multiset(M) \<Longrightarrow> M +# {#a#} -# {#a#} = M"
-apply (unfold multiset_def munion_def mdiff_def msingle_def normalize_def mset_of_def)
+  unfolding multiset_def munion_def mdiff_def msingle_def normalize_def mset_of_def
 apply (auto cong add: if_cong simp add: ltD multiset_fun_iff funrestrict_def subset_Un_iff2 [THEN iffD1])
 prefer 2 apply (force intro!: lam_type)
 apply (subgoal_tac [2] "{x \<in> A \<union> {a} . x \<noteq> a \<and> x \<in> A} = A")
@@ -483,7 +483,7 @@
   unfolding multiset_def
 apply (erule Finite_induct)
 apply (auto simp add: multiset_fun_iff)
-apply (unfold mset_of_def mcount_def)
+  unfolding mset_of_def mcount_def
 apply (case_tac "x \<in> A", auto)
 apply (subgoal_tac "$# M ` x $+ #-1 = $# M ` x $- $# 1")
 apply (erule ssubst)
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/Induct/Ntree.thy
--- a/src/ZF/Induct/Ntree.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Induct/Ntree.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -85,7 +85,7 @@
 \<close>
 
 lemma ntree_mono: "A \<subseteq> B \<Longrightarrow> ntree(A) \<subseteq> ntree(B)"
-  apply (unfold ntree.defs)
+    unfolding ntree.defs
   apply (rule lfp_mono)
     apply (rule ntree.bnd_mono)+
   apply (assumption | rule univ_mono basic_monos)+
@@ -93,7 +93,7 @@
 
 lemma ntree_univ: "ntree(univ(A)) \<subseteq> univ(A)"
   \<comment> \<open>Easily provable by induction also\<close>
-  apply (unfold ntree.defs ntree.con_defs)
+    unfolding ntree.defs ntree.con_defs
   apply (rule lfp_lowerbound)
    apply (rule_tac [2] A_subset_univ [THEN univ_mono])
   apply (blast intro: Pair_in_univ nat_fun_univ [THEN subsetD])
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/Induct/PropLog.thy
--- a/src/ZF/Induct/PropLog.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Induct/PropLog.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -107,7 +107,7 @@
 subsection \<open>Proof theory of propositional logic\<close>
 
 lemma thms_mono: "G \<subseteq> H \<Longrightarrow> thms(G) \<subseteq> thms(H)"
-  apply (unfold thms.defs)
+    unfolding thms.defs
   apply (rule lfp_mono)
     apply (rule thms.bnd_mono)+
   apply (assumption | rule univ_mono basic_monos)+
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/Induct/Rmap.thy
--- a/src/ZF/Induct/Rmap.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Induct/Rmap.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -21,7 +21,7 @@
   type_intros domainI rangeI list.intros
 
 lemma rmap_mono: "r \<subseteq> s \<Longrightarrow> rmap(r) \<subseteq> rmap(s)"
-  apply (unfold rmap.defs)
+    unfolding rmap.defs
   apply (rule lfp_mono)
     apply (rule rmap.bnd_mono)+
   apply (assumption | rule Sigma_mono list_mono domain_mono range_mono basic_monos)+
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/Induct/Term.thy
--- a/src/ZF/Induct/Term.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Induct/Term.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -77,7 +77,7 @@
 \<close>
 
 lemma term_mono: "A \<subseteq> B \<Longrightarrow> term(A) \<subseteq> term(B)"
-  apply (unfold term.defs)
+    unfolding term.defs
   apply (rule lfp_mono)
     apply (rule term.bnd_mono)+
   apply (rule univ_mono basic_monos| assumption)+
@@ -85,7 +85,7 @@
 
 lemma term_univ: "term(univ(A)) \<subseteq> univ(A)"
   \<comment> \<open>Easily provable by induction also\<close>
-  apply (unfold term.defs term.con_defs)
+    unfolding term.defs term.con_defs
   apply (rule lfp_lowerbound)
    apply (rule_tac [2] A_subset_univ [THEN univ_mono])
   apply safe
@@ -120,7 +120,7 @@
   term_rec(Apply(a,ts), d) = d(a, ts, map (\<lambda>z. term_rec(z,d), ts))"
   \<comment> \<open>Typing premise is necessary to invoke \<open>map_lemma\<close>.\<close>
   apply (rule term_rec_def [THEN def_Vrec, THEN trans])
-  apply (unfold term.con_defs)
+    unfolding term.con_defs
   apply (simp add: rank_pair2 map_lemma)
   done
 
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/Induct/Tree_Forest.thy
--- a/src/ZF/Induct/Tree_Forest.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Induct/Tree_Forest.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -39,7 +39,7 @@
 \<close>
 
 lemma tree_subset_TF: "tree(A) \<subseteq> tree_forest(A)"
-  apply (unfold tree_forest.defs)
+    unfolding tree_forest.defs
   apply (rule Part_subset)
   done
 
@@ -47,7 +47,7 @@
   by (rule tree_subset_TF [THEN subsetD])
 
 lemma forest_subset_TF: "forest(A) \<subseteq> tree_forest(A)"
-  apply (unfold tree_forest.defs)
+    unfolding tree_forest.defs
   apply (rule Part_subset)
   done
 
@@ -63,7 +63,7 @@
   "tree_forest(A) = (A \<times> forest(A)) + ({0} + tree(A) \<times> forest(A))"
     \<comment> \<open>NOT useful, but interesting \dots\<close>
   supply rews = tree_forest.con_defs tree_def forest_def
-  apply (unfold tree_def forest_def)
+    unfolding tree_def forest_def
   apply (fast intro!: tree_forest.intros [unfolded rews, THEN PartD1]
     elim: tree_forest.cases [unfolded rews])
   done
@@ -75,13 +75,13 @@
   by (rule tree_forest_unfold [unfolded tree_def forest_def])
 
 lemma tree_unfold: "tree(A) = {Inl(x). x \<in> A \<times> forest(A)}"
-  apply (unfold tree_def forest_def)
+    unfolding tree_def forest_def
   apply (rule Part_Inl [THEN subst])
   apply (rule tree_forest_unfold' [THEN subst_context])
   done
 
 lemma forest_unfold: "forest(A) = {Inr(x). x \<in> {0} + tree(A)*forest(A)}"
-  apply (unfold tree_def forest_def)
+    unfolding tree_def forest_def
   apply (rule Part_Inr [THEN subst])
   apply (rule tree_forest_unfold' [THEN subst_context])
   done
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/List.thy
--- a/src/ZF/List.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/List.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -154,7 +154,7 @@
 (**  Lemmas to justify using "list" in other recursive type definitions **)
 
 lemma list_mono: "A<=B \<Longrightarrow> list(A) \<subseteq> list(B)"
-apply (unfold list.defs )
+  unfolding list.defs 
 apply (rule lfp_mono)
 apply (simp_all add: list.bnd_mono)
 apply (assumption | rule univ_mono basic_monos)+
@@ -162,7 +162,7 @@
 
 (*There is a similar proof by list induction.*)
 lemma list_univ: "list(univ(A)) \<subseteq> univ(A)"
-apply (unfold list.defs list.con_defs)
+  unfolding list.defs list.con_defs
 apply (rule lfp_lowerbound)
 apply (rule_tac [2] A_subset_univ [THEN univ_mono])
 apply (blast intro!: zero_in_univ Inl_in_univ Inr_in_univ Pair_in_univ)
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/Order.thy
--- a/src/ZF/Order.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Order.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -362,7 +362,7 @@
 
 lemma well_ord_ord_iso:
     "\<lbrakk>well_ord(B,s);  f \<in> ord_iso(A,r,B,s)\<rbrakk> \<Longrightarrow> well_ord(A,r)"
-apply (unfold well_ord_def tot_ord_def)
+  unfolding well_ord_def tot_ord_def
 apply (fast elim!: part_ord_ord_iso linear_ord_iso wf_on_ord_iso)
 done
 
@@ -409,7 +409,7 @@
 (*Does not assume r is a wellordering!*)
 lemma ord_iso_image_pred:
      "\<lbrakk>f \<in> ord_iso(A,r,B,s);  a \<in> A\<rbrakk> \<Longrightarrow> f `` pred(A,a,r) = pred(B, f`a, s)"
-apply (unfold ord_iso_def pred_def)
+  unfolding ord_iso_def pred_def
 apply (erule CollectE)
 apply (simp (no_asm_simp) add: image_fun [OF bij_is_fun Collect_subset])
 apply (rule equalityI)
@@ -500,7 +500,7 @@
 
 lemma function_ord_iso_map:
     "well_ord(B,s) \<Longrightarrow> function(ord_iso_map(A,r,B,s))"
-apply (unfold ord_iso_map_def function_def)
+  unfolding ord_iso_map_def function_def
 apply (blast intro: well_ord_iso_pred_eq ord_iso_sym ord_iso_trans)
 done
 
@@ -567,7 +567,7 @@
       \<Longrightarrow> domain(ord_iso_map(A,r,B,s)) = A |
           (\<exists>x\<in>A. domain(ord_iso_map(A,r,B,s)) = pred(A,x,r))"
 apply (frule well_ord_is_wf)
-apply (unfold wf_on_def wf_def)
+  unfolding wf_on_def wf_def
 apply (drule_tac x = "A-domain (ord_iso_map (A,r,B,s))" in spec)
 apply safe
 (*The first case: the domain equals A*)
@@ -642,7 +642,7 @@
 
 lemma well_ord_imp_ex1_first:
         "\<lbrakk>well_ord(A,r); B<=A; B\<noteq>0\<rbrakk> \<Longrightarrow> (\<exists>!b. first(b,B,r))"
-apply (unfold well_ord_def wf_on_def wf_def first_def)
+  unfolding well_ord_def wf_on_def wf_def first_def
 apply (elim conjE allE disjE, blast)
 apply (erule bexE)
 apply (rule_tac a = x in ex1I, auto)
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/OrderArith.thy
--- a/src/ZF/OrderArith.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/OrderArith.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -325,13 +325,13 @@
 
 lemma irrefl_rvimage:
     "\<lbrakk>f \<in> inj(A,B);  irrefl(B,r)\<rbrakk> \<Longrightarrow> irrefl(A, rvimage(A,f,r))"
-apply (unfold irrefl_def rvimage_def)
+  unfolding irrefl_def rvimage_def
 apply (blast intro: inj_is_fun [THEN apply_type])
 done
 
 lemma trans_on_rvimage:
     "\<lbrakk>f \<in> inj(A,B);  trans[B](r)\<rbrakk> \<Longrightarrow> trans[A](rvimage(A,f,r))"
-apply (unfold trans_on_def rvimage_def)
+  unfolding trans_on_def rvimage_def
 apply (blast intro: inj_is_fun [THEN apply_type])
 done
 
@@ -384,7 +384,7 @@
 lemma well_ord_rvimage:
      "\<lbrakk>f \<in> inj(A,B);  well_ord(B,r)\<rbrakk> \<Longrightarrow> well_ord(A, rvimage(A,f,r))"
 apply (rule well_ordI)
-apply (unfold well_ord_def tot_ord_def)
+  unfolding well_ord_def tot_ord_def
 apply (blast intro!: wf_on_rvimage inj_is_fun)
 apply (blast intro!: linear_rvimage)
 done
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/OrderType.thy
--- a/src/ZF/OrderType.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/OrderType.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -99,7 +99,7 @@
 
 lemma ordermap_type:
     "ordermap(A,r) \<in> A -> ordertype(A,r)"
-apply (unfold ordermap_def ordertype_def)
+  unfolding ordermap_def ordertype_def
 apply (rule lam_type)
 apply (rule lamI [THEN imageI], assumption+)
 done
@@ -110,7 +110,7 @@
 lemma ordermap_eq_image:
     "\<lbrakk>wf[A](r);  x \<in> A\<rbrakk>
      \<Longrightarrow> ordermap(A,r) ` x = ordermap(A,r) `` pred(A,x,r)"
-apply (unfold ordermap_def pred_def)
+  unfolding ordermap_def pred_def
 apply (simp (no_asm_simp))
 apply (erule wfrec_on [THEN trans], assumption)
 apply (simp (no_asm_simp) add: subset_iff image_lam vimage_singleton_iff)
@@ -149,7 +149,7 @@
 apply (rule_tac a=x in wf_on_induct, assumption+)
 apply (simp (no_asm_simp) add: ordermap_pred_unfold)
 apply (rule OrdI [OF _ Ord_is_Transset])
-apply (unfold pred_def Transset_def)
+  unfolding pred_def Transset_def
 apply (blast intro: trans_onD
              dest!: ordermap_unfold [THEN equalityD1])+
 done
@@ -160,7 +160,7 @@
 apply (subst image_fun [OF ordermap_type subset_refl])
 apply (rule OrdI [OF _ Ord_is_Transset])
 prefer 2 apply (blast intro: Ord_ordermap)
-apply (unfold Transset_def well_ord_def)
+  unfolding Transset_def well_ord_def
 apply (blast intro: trans_onD
              dest!: ordermap_unfold [THEN equalityD1])
 done
@@ -190,7 +190,7 @@
 
 lemma ordermap_bij:
     "well_ord(A,r) \<Longrightarrow> ordermap(A,r) \<in> bij(A, ordertype(A,r))"
-apply (unfold well_ord_def tot_ord_def bij_def inj_def)
+  unfolding well_ord_def tot_ord_def bij_def inj_def
 apply (force intro!: ordermap_type ordermap_surj
              elim: linearE dest: ordermap_mono
              simp add: mem_not_refl)
@@ -381,7 +381,7 @@
  "b \<in> B \<Longrightarrow>
          id(A+pred(B,b,s))
          \<in> bij(A+pred(B,b,s), pred(A+B, Inr(b), radd(A,r,B,s)))"
-apply (unfold pred_def id_def)
+  unfolding pred_def id_def
 apply (rule_tac d = "\<lambda>z. z" in lam_bijective, auto)
 done
 
@@ -780,7 +780,7 @@
      \<Longrightarrow> ordertype(pred(i*j, <i',j'>, rmult(i,Memrel(i),j,Memrel(j))),
                    rmult(i,Memrel(i),j,Memrel(j))) =
          raw_oadd (j**i', j')"
-apply (unfold raw_oadd_def omult_def)
+  unfolding raw_oadd_def omult_def
 apply (simp add: ordertype_pred_Pair_eq lt_pred_Memrel ltD lt_Ord2
                  well_ord_Memrel)
 apply (rule trans)
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/Perm.thy
--- a/src/ZF/Perm.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Perm.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -177,7 +177,7 @@
 lemmas id_inj = subset_refl [THEN id_subset_inj]
 
 lemma id_surj: "id(A): surj(A,A)"
-apply (unfold id_def surj_def)
+  unfolding id_def surj_def
 apply (simp (no_asm_simp))
 done
 
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/QUniv.thy
--- a/src/ZF/QUniv.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/QUniv.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -122,7 +122,7 @@
 (*The opposite inclusion*)
 lemma quniv_QPair_D:
     "<a;b> \<in> quniv(A) \<Longrightarrow> a: quniv(A) \<and> b: quniv(A)"
-apply (unfold quniv_def QPair_def)
+  unfolding quniv_def QPair_def
 apply (rule Transset_includes_summands [THEN conjE])
 apply (rule Transset_eclose [THEN Transset_univ])
 apply (erule PowD, blast)
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/Resid/Confluence.thy
--- a/src/ZF/Resid/Confluence.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Resid/Confluence.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -22,7 +22,7 @@
 
 lemma strip_lemma_r: 
     "\<lbrakk>confluence(Spar_red1)\<rbrakk>\<Longrightarrow> strip"
-apply (unfold confluence_def strip_def)
+  unfolding confluence_def strip_def
 apply (rule impI [THEN allI, THEN allI])
 apply (erule Spar_red.induct, fast)
 apply (fast intro: Spar_red.trans)
@@ -31,7 +31,7 @@
 
 lemma strip_lemma_l: 
     "strip\<Longrightarrow> confluence(Spar_red)"
-apply (unfold confluence_def strip_def)
+  unfolding confluence_def strip_def
 apply (rule impI [THEN allI, THEN allI])
 apply (erule Spar_red.induct, blast)
 apply clarify
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/Trancl.thy
--- a/src/ZF/Trancl.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Trancl.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -196,7 +196,7 @@
 
 (*Transitivity of r^+ is proved by transitivity of r^*  *)
 lemma trans_trancl: "trans(r^+)"
-apply (unfold trans_def trancl_def)
+  unfolding trans_def trancl_def
 apply (blast intro: rtrancl_into_rtrancl
                     trans_rtrancl [THEN transD, THEN compI])
 done
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/UNITY/AllocBase.thy
--- a/src/ZF/UNITY/AllocBase.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/UNITY/AllocBase.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -268,7 +268,7 @@
 
 
 lemma part_ord_Lt [simp]: "part_ord(nat, Lt)"
-apply (unfold part_ord_def Lt_def irrefl_def trans_on_def)
+  unfolding part_ord_def Lt_def irrefl_def trans_on_def
 apply (auto intro: lt_trans)
 done
 
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/UNITY/ClientImpl.thy
--- a/src/ZF/UNITY/ClientImpl.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/UNITY/ClientImpl.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -210,7 +210,7 @@
 
 lemma strict_prefix_is_prefix:
     "\<langle>xs, ys\<rangle> \<in> strict_prefix(A) \<longleftrightarrow>  \<langle>xs, ys\<rangle> \<in> prefix(A) \<and> xs\<noteq>ys"
-apply (unfold strict_prefix_def id_def lam_def)
+  unfolding strict_prefix_def id_def lam_def
 apply (auto dest: prefix_type [THEN subsetD])
 done
 
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/UNITY/Comp.thy
--- a/src/ZF/UNITY/Comp.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/UNITY/Comp.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -144,7 +144,7 @@
 (*** preserves ***)
 
 lemma preserves_is_safety_prop [simp]: "safety_prop(preserves(f))"
-apply (unfold preserves_def safety_prop_def)
+  unfolding preserves_def safety_prop_def
 apply (auto dest: ActsD simp add: stable_def constrains_def)
 apply (drule_tac c = act in subsetD, auto)
 done
@@ -157,7 +157,7 @@
 
 lemma preserves_imp_eq: 
      "\<lbrakk>F \<in> preserves(f);  act \<in> Acts(F);  \<langle>s,t\<rangle> \<in> act\<rbrakk> \<Longrightarrow> f(s) = f(t)"
-apply (unfold preserves_def stable_def constrains_def)
+  unfolding preserves_def stable_def constrains_def
 apply (subgoal_tac "s \<in> state \<and> t \<in> state")
  prefer 2 apply (blast dest!: Acts_type [THEN subsetD], force) 
 done
@@ -224,7 +224,7 @@
 
 lemma preserves_imp_increasing: 
  "\<lbrakk>F \<in> preserves(f); \<forall>x \<in> state. f(x):A\<rbrakk> \<Longrightarrow> F \<in> Increasing.increasing(A, r, f)"
-apply (unfold Increasing.increasing_def)
+  unfolding Increasing.increasing_def
 apply (auto intro: preserves_into_program)
 apply (rule_tac P = "\<lambda>x. \<langle>k, x\<rangle>:r" in preserves_imp_stable, auto)
 done
@@ -324,7 +324,7 @@
      \<forall>k \<in> A. F \<squnion> G \<in> Stable({s \<in> state. P(k, g(s))});  
      G \<in> preserves(f); \<forall>s \<in> state. f(s):A\<rbrakk>
   \<Longrightarrow> F \<squnion> G \<in> Stable({s \<in> state. P(f(s), g(s))})"
-apply (unfold stable_def Stable_def preserves_def)
+  unfolding stable_def Stable_def preserves_def
 apply (rule_tac A = "(\<Union>k \<in> A. {s \<in> state. f(s)=k} \<inter> {s \<in> state. P (f (s), g (s))})" in Constrains_weaken_L)
 prefer 2 apply blast
 apply (rule Constrains_UN_left, auto)
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/UNITY/Constrains.thy
--- a/src/ZF/UNITY/Constrains.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/UNITY/Constrains.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -103,7 +103,7 @@
 (*The set of all reachable states is an invariant...*)
 lemma invariant_reachable: 
    "F \<in> program \<Longrightarrow> F \<in> invariant(reachable(F))"
-apply (unfold invariant_def initially_def)
+  unfolding invariant_def initially_def
 apply (blast intro: reachable_type [THEN subsetD] reachable.intros)
 done
 
@@ -239,7 +239,7 @@
 lemma stable_imp_Stable: 
 "F \<in> stable(A) \<Longrightarrow> F \<in> Stable(A)"
 
-apply (unfold stable_def Stable_def)
+  unfolding stable_def Stable_def
 apply (erule constrains_imp_Constrains)
 done
 
@@ -340,7 +340,7 @@
 lemma AlwaysI: 
 "\<lbrakk>Init(F)<=A;  F \<in> Stable(A)\<rbrakk> \<Longrightarrow> F \<in> Always(A)"
 
-apply (unfold Always_def initially_def)
+  unfolding Always_def initially_def
 apply (frule Stable_type [THEN subsetD], auto)
 done
 
@@ -360,7 +360,7 @@
 
 lemma invariant_imp_Always: 
      "F \<in> invariant(A) \<Longrightarrow> F \<in> Always(A)"
-apply (unfold Always_def invariant_def Stable_def stable_def)
+  unfolding Always_def invariant_def Stable_def stable_def
 apply (blast intro: constrains_imp_Constrains)
 done
 
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/UNITY/FP.thy
--- a/src/ZF/UNITY/FP.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/UNITY/FP.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -51,7 +51,7 @@
 apply (subgoal_tac "FP (F) \<inter> B = (\<Union>x\<in>B. FP (F) \<inter> {x}) ")
  prefer 2 apply blast
 apply (simp (no_asm_simp) add: Int_cons_right)
-apply (unfold FP_def stable_def)
+  unfolding FP_def stable_def
 apply (rule constrains_UN)
 apply (auto simp add: cons_absorb)
 done
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/UNITY/Follows.thy
--- a/src/ZF/UNITY/Follows.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/UNITY/Follows.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -53,7 +53,7 @@
 lemma subset_Always_comp:
 "\<lbrakk>mono1(A, r, B, s, h); \<forall>x \<in> state. f(x):A \<and> g(x):A\<rbrakk> \<Longrightarrow>
    Always({x \<in> state. <f(x), g(x)> \<in> r})<=Always({x \<in> state. <(h comp f)(x), (h comp g)(x)> \<in> s})"
-apply (unfold mono1_def metacomp_def)
+  unfolding mono1_def metacomp_def
 apply (auto simp add: Always_eq_includes_reachable)
 done
 
@@ -110,7 +110,7 @@
   mono2(A, r, B, s, C, t, h); refl(A, r); refl(B, s); trans[C](t);
   \<forall>x \<in> state. f1(x):A \<and> f(x):A \<and> g(x):B; k \<in> C\<rbrakk> \<Longrightarrow>
   F:{x \<in> state. <k, h(f(x), g(x))> \<in> t} \<longmapsto>w {x \<in> state. <k, h(f1(x), g(x))> \<in> t}"
-apply (unfold mono2_def Increasing_def)
+  unfolding mono2_def Increasing_def
 apply (rule single_LeadsTo_I, auto)
 apply (drule_tac x = "g (sa) " and A = B in bspec)
 apply auto
@@ -133,7 +133,7 @@
   mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t);
   \<forall>x \<in> state. f(x):A \<and> g1(x):B \<and> g(x):B; k \<in> C\<rbrakk> \<Longrightarrow>
   F:{x \<in> state. <k, h(f(x), g(x))> \<in> t} \<longmapsto>w {x \<in> state. <k, h(f(x), g1(x))> \<in> t}"
-apply (unfold mono2_def Increasing_def)
+  unfolding mono2_def Increasing_def
 apply (rule single_LeadsTo_I, auto)
 apply (drule_tac x = "f (sa) " and P = "\<lambda>k. F \<in> Stable (X (k))" for X in bspec)
 apply auto
@@ -275,7 +275,7 @@
 lemma Always_Follows1:
 "\<lbrakk>F \<in> Always({s \<in> state. f(s) = g(s)}); F \<in> Follows(A, r, f, h);
     \<forall>x \<in> state. g(x):A\<rbrakk> \<Longrightarrow> F \<in> Follows(A, r, g, h)"
-apply (unfold Follows_def Increasing_def Stable_def)
+  unfolding Follows_def Increasing_def Stable_def
 apply (simp add: INT_iff, auto)
 apply (rule_tac [3] C = "{s \<in> state. f(s)=g(s)}"
         and A = "{s \<in> state. <k, h (s)> \<in> r}"
@@ -293,7 +293,7 @@
 lemma Always_Follows2:
 "\<lbrakk>F \<in> Always({s \<in> state. g(s) = h(s)});
   F \<in> Follows(A, r, f, g); \<forall>x \<in> state. h(x):A\<rbrakk> \<Longrightarrow> F \<in> Follows(A, r, f, h)"
-apply (unfold Follows_def Increasing_def Stable_def)
+  unfolding Follows_def Increasing_def Stable_def
 apply (simp add: INT_iff, auto)
 apply (rule_tac [3] C = "{s \<in> state. g (s) =h (s) }"
             and A = "{s \<in> state. <k, g (s) > \<in> r}"
@@ -352,7 +352,7 @@
 
 lemma MultLe_refl1 [simp]:
  "\<lbrakk>multiset(M); mset_of(M)<=A\<rbrakk> \<Longrightarrow> \<langle>M, M\<rangle> \<in> MultLe(A, r)"
-apply (unfold MultLe_def id_def lam_def)
+  unfolding MultLe_def id_def lam_def
 apply (auto simp add: Mult_iff_multiset)
 done
 
@@ -361,7 +361,7 @@
 
 
 lemma trans_on_MultLe [simp]: "trans[Mult(A)](MultLe(A,r))"
-apply (unfold MultLe_def trans_on_def)
+  unfolding MultLe_def trans_on_def
 apply (auto intro: trancl_trans simp add: multirel_def)
 done
 
@@ -379,7 +379,7 @@
 
 lemma part_order_imp_part_ord:
      "part_order(A, r) \<Longrightarrow> part_ord(A, r-id(A))"
-apply (unfold part_order_def part_ord_def)
+  unfolding part_order_def part_ord_def
 apply (simp add: refl_def id_def lam_def irrefl_def, auto)
 apply (simp (no_asm) add: trans_on_def)
 apply auto
@@ -390,7 +390,7 @@
 
 lemma antisym_MultLe [simp]:
   "part_order(A, r) \<Longrightarrow> antisym(MultLe(A,r))"
-apply (unfold MultLe_def antisym_def)
+  unfolding MultLe_def antisym_def
 apply (drule part_order_imp_part_ord, auto)
 apply (drule irrefl_on_multirel)
 apply (frule multirel_type [THEN subsetD])
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/UNITY/GenPrefix.thy
--- a/src/ZF/UNITY/GenPrefix.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/UNITY/GenPrefix.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -588,13 +588,13 @@
 declare refl_Ge [iff]
 
 lemma antisym_Ge: "antisym(Ge)"
-apply (unfold antisym_def Ge_def)
+  unfolding antisym_def Ge_def
 apply (auto intro: le_anti_sym)
 done
 declare antisym_Ge [iff]
 
 lemma trans_Ge: "trans(Ge)"
-apply (unfold trans_def Ge_def)
+  unfolding trans_def Ge_def
 apply (auto intro: le_trans)
 done
 declare trans_Ge [iff]
@@ -611,7 +611,7 @@
 
 lemma prefix_imp_pfixGe:
   "\<langle>xs,ys\<rangle>:prefix(nat) \<Longrightarrow> xs pfixGe ys"
-apply (unfold prefix_def Ge_def)
+  unfolding prefix_def Ge_def
 apply (rule gen_prefix_mono [THEN subsetD], auto)
 done
 (* Added by Sidi \<in> prefix and take *)
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/UNITY/Increasing.thy
--- a/src/ZF/UNITY/Increasing.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/UNITY/Increasing.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -48,7 +48,7 @@
 
 lemma increasing_constant [simp]: 
  "F \<in> increasing[A](r, \<lambda>s. c) \<longleftrightarrow> F \<in> program \<and> c \<in> A"
-apply (unfold increasing_def stable_def)
+  unfolding increasing_def stable_def
 apply (subgoal_tac "\<exists>x. x \<in> state")
 apply (auto dest: stable_type [THEN subsetD] intro: st0_in_state)
 done
@@ -94,7 +94,7 @@
 lemma increasing_imp_Increasing: 
      "F \<in> increasing[A](r, f) \<Longrightarrow> F \<in> Increasing[A](r, f)"
 
-apply (unfold increasing_def Increasing_def)
+  unfolding increasing_def Increasing_def
 apply (auto intro: stable_imp_Stable)
 done
 
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/UNITY/Monotonicity.thy
--- a/src/ZF/UNITY/Monotonicity.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/UNITY/Monotonicity.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -109,7 +109,7 @@
 
 lemma mono_munion [iff]: 
      "mono2(Mult(A), MultLe(A,r), Mult(A), MultLe(A, r), Mult(A), MultLe(A, r), munion)"
-apply (unfold mono2_def MultLe_def)
+  unfolding mono2_def MultLe_def
 apply (auto simp add: Mult_iff_multiset)
 apply (blast intro: munion_multirel_mono munion_multirel_mono1 munion_multirel_mono2 multiset_into_Mult)+
 done
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/UNITY/UNITY.thy
--- a/src/ZF/UNITY/UNITY.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/UNITY/UNITY.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -567,7 +567,7 @@
 done
 
 lemma invariantI: "\<lbrakk>Init(F)\<subseteq>A;  F \<in> stable(A)\<rbrakk> \<Longrightarrow> F \<in> invariant(A)"
-apply (unfold invariant_def initially_def)
+  unfolding invariant_def initially_def
 apply (frule stable_type [THEN subsetD], auto)
 done
 
@@ -583,7 +583,7 @@
       \<^term>\<open>invariant(A) \<inter> invariant(B) \<subseteq> invariant (A \<inter> B)\<close>\<close>
 lemma invariant_Int:
   "\<lbrakk>F \<in> invariant(A);  F \<in> invariant(B)\<rbrakk> \<Longrightarrow> F \<in> invariant(A \<inter> B)"
-apply (unfold invariant_def initially_def)
+  unfolding invariant_def initially_def
 apply (simp add: stable_Int, blast)
 done
 
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/UNITY/Union.thy
--- a/src/ZF/UNITY/Union.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/UNITY/Union.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -121,7 +121,7 @@
 by auto
 
 lemma Join_SKIP_left [simp]: "SKIP \<squnion> F = programify(F)"
-apply (unfold Join_def SKIP_def)
+  unfolding Join_def SKIP_def
 apply (auto simp add: Int_absorb cons_eq)
 done
 
@@ -364,7 +364,7 @@
 lemma stable_Join_constrains:
     "\<lbrakk>F \<in> stable(A);  G \<in> A co A'\<rbrakk>
      \<Longrightarrow> F \<squnion> G \<in> A co A'"
-apply (unfold stable_def constrains_def Join_def st_set_def)
+  unfolding stable_def constrains_def Join_def st_set_def
 apply (cut_tac F = F in Acts_type)
 apply (cut_tac F = G in Acts_type, force)
 done
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/UNITY/WFair.thy
--- a/src/ZF/UNITY/WFair.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/UNITY/WFair.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -165,13 +165,13 @@
 
 lemma leadsToD2:
 "F \<in> A \<longmapsto> B \<Longrightarrow> F \<in> program \<and> st_set(A) \<and> st_set(B)"
-apply (unfold leadsTo_def st_set_def)
+  unfolding leadsTo_def st_set_def
 apply (blast dest: leads_left leads_right)
 done
 
 lemma leadsTo_Basis:
     "\<lbrakk>F \<in> A ensures B; st_set(A); st_set(B)\<rbrakk> \<Longrightarrow> F \<in> A \<longmapsto> B"
-apply (unfold leadsTo_def st_set_def)
+  unfolding leadsTo_def st_set_def
 apply (cut_tac ensures_type)
 apply (auto intro: leads.Basis)
 done
@@ -204,14 +204,14 @@
 lemma leadsTo_Union:
     "\<lbrakk>\<And>A. A \<in> S \<Longrightarrow> F \<in> A \<longmapsto> B; F \<in> program; st_set(B)\<rbrakk>
      \<Longrightarrow> F \<in> \<Union>(S) \<longmapsto> B"
-apply (unfold leadsTo_def st_set_def)
+  unfolding leadsTo_def st_set_def
 apply (blast intro: leads.Union dest: leads_left)
 done
 
 lemma leadsTo_Union_Int:
     "\<lbrakk>\<And>A. A \<in> S \<Longrightarrow>F \<in> (A \<inter> C) \<longmapsto> B; F \<in> program; st_set(B)\<rbrakk>
      \<Longrightarrow> F \<in> (\<Union>(S)Int C)\<longmapsto> B"
-apply (unfold leadsTo_def st_set_def)
+  unfolding leadsTo_def st_set_def
 apply (simp only: Int_Union_Union)
 apply (blast dest: leads_left intro: leads.Union)
 done
@@ -441,7 +441,7 @@
 
 lemma psp_ensures:
 "\<lbrakk>F \<in> A ensures A'; F \<in> B co B'\<rbrakk>\<Longrightarrow> F: (A \<inter> B') ensures ((A' \<inter> B) \<union> (B' - B))"
-apply (unfold ensures_def constrains_def st_set_def)
+  unfolding ensures_def constrains_def st_set_def
 (*speeds up the proof*)
 apply clarify
 apply (blast intro: transient_strengthen)
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/WF.thy
--- a/src/ZF/WF.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/WF.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -82,7 +82,7 @@
 lemma wf_onI:
  assumes prem: "\<And>Z u. \<lbrakk>Z<=A;  u \<in> Z;  \<forall>x\<in>Z. \<exists>y\<in>Z. \<langle>y,x\<rangle>:r\<rbrakk> \<Longrightarrow> False"
  shows         "wf[A](r)"
-apply (unfold wf_on_def wf_def)
+  unfolding wf_on_def wf_def
 apply (rule equals0I [THEN disjCI, THEN allI])
 apply (rule_tac Z = Z in prem, blast+)
 done
@@ -287,7 +287,7 @@
 apply (rename_tac a1)
 apply (rule_tac f = "\<lambda>y\<in>r-``{a1}. wftrec (r,y,H)" in is_the_recfun)
   apply typecheck
-apply (unfold is_recfun_def wftrec_def)
+  unfolding is_recfun_def wftrec_def
   \<comment> \<open>Applying the substitution: must keep the quantified assumption!\<close>
 apply (rule lam_cong [OF refl])
 apply (drule underD)
@@ -359,7 +359,7 @@
 lemma wfrec_on:
  "\<lbrakk>wf[A](r);  a \<in> A\<rbrakk> \<Longrightarrow>
          wfrec[A](r,a,H) = H(a, \<lambda>x\<in>(r-``{a}) \<inter> A. wfrec[A](r,x,H))"
-apply (unfold wf_on_def wfrec_on_def)
+  unfolding wf_on_def wfrec_on_def
 apply (erule wfrec [THEN trans])
 apply (simp add: vimage_Int_square cons_subset_iff)
 done
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/ZF_Base.thy
--- a/src/ZF/ZF_Base.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/ZF_Base.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -393,7 +393,7 @@
 (*Useful for proving A<=B by rewriting in some cases*)
 lemma subset_iff:
      "A<=B <-> (\<forall>x. x\<in>A \<longrightarrow> x\<in>B)"
-apply (unfold subset_def Ball_def)
+  unfolding subset_def Ball_def
 apply (rule iff_refl)
 done
 
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/Zorn.thy
--- a/src/ZF/Zorn.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/Zorn.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -312,7 +312,7 @@
 apply (rule ccontr)
 apply (frule_tac z=z in chain_extend)
   apply (assumption, blast)
-apply (unfold maxchain_def super_def)
+  unfolding maxchain_def super_def
 apply (blast elim!: equalityCE)
 done
 
@@ -346,7 +346,7 @@
      "next \<in> increasing(S) 
       \<Longrightarrow> well_ord(TFin(S,next), Subset_rel(TFin(S,next)))"
 apply (rule well_ordI)
-apply (unfold Subset_rel_def linear_def)
+  unfolding Subset_rel_def linear_def
 txt\<open>Prove the well-foundedness goal\<close>
 apply (rule wf_onI)
 apply (frule well_ord_TFin_lemma, assumption)
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/ex/CoUnit.thy
--- a/src/ZF/ex/CoUnit.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/ex/CoUnit.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -37,7 +37,7 @@
   apply (rule subsetI)
   apply (erule counit.coinduct)
    apply (rule subset_refl)
-  apply (unfold counit.con_defs)
+    unfolding counit.con_defs
   apply fast
   done
 
@@ -60,7 +60,7 @@
   by (fast elim!: counit2.free_elims)
 
 lemma Con2_bnd_mono: "bnd_mono(univ(0), \<lambda>x. Con2(x, x))"
-  apply (unfold counit2.con_defs)
+    unfolding counit2.con_defs
   apply (rule bnd_monoI)
    apply (assumption | rule subset_refl QPair_subset_univ QPair_mono)+
   done
@@ -79,7 +79,7 @@
   apply (tactic "safe_tac (put_claset subset_cs \<^context>)")
   apply (erule counit2.cases)
   apply (erule counit2.cases)
-  apply (unfold counit2.con_defs)
+    unfolding counit2.con_defs
   apply (tactic \<open>fast_tac (put_claset subset_cs \<^context>
     addSIs [@{thm QPair_Int_Vset_subset_UN} RS @{thm subset_trans}, @{thm QPair_mono}]
     addSEs [@{thm Ord_in_Ord}, @{thm Pair_inject}]) 1\<close>)
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/ex/Commutation.thy
--- a/src/ZF/ex/Commutation.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/ex/Commutation.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -52,7 +52,7 @@
 (* A special case of square_rtrancl_on *)
 lemma diamond_strip:
   "diamond(r) \<Longrightarrow> strip(r)"
-apply (unfold diamond_def commute_def strip_def)
+  unfolding diamond_def commute_def strip_def
 apply (rule square_rtrancl, simp_all)
 done
 
@@ -74,7 +74,7 @@
 by (simp add: confluent_def)
 
 lemma strip_confluent: "strip(r) \<Longrightarrow> confluent(r)"
-apply (unfold strip_def confluent_def diamond_def)
+  unfolding strip_def confluent_def diamond_def
 apply (drule commute_rtrancl)
 apply (simp_all add: rtrancl_field)
 done
@@ -88,7 +88,7 @@
 
 lemma diamond_confluent:
     "diamond(r) \<Longrightarrow> confluent(r)"
-apply (unfold diamond_def confluent_def)
+  unfolding diamond_def confluent_def
 apply (erule commute_rtrancl, simp)
 done
 
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/ex/Group.thy
--- a/src/ZF/ex/Group.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/ex/Group.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -154,7 +154,7 @@
 lemma (in group) inv [simp]:
   "x \<in> carrier(G) \<Longrightarrow> inv x \<in> carrier(G) \<and> inv x \<cdot> x = \<one> \<and> x \<cdot> inv x = \<one>"
   apply (frule inv_ex)
-  apply (unfold Bex_def m_inv_def)
+    unfolding Bex_def m_inv_def
   apply (erule exE)
   apply (rule theI)
   apply (rule ex1I, assumption)
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/ex/LList.thy
--- a/src/ZF/ex/LList.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/ex/LList.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -91,7 +91,7 @@
 (*** Lemmas to justify using "llist" in other recursive type definitions ***)
 
 lemma llist_mono: "A \<subseteq> B \<Longrightarrow> llist(A) \<subseteq> llist(B)"
-apply (unfold llist.defs )
+  unfolding llist.defs 
 apply (rule gfp_mono)
 apply (rule llist.bnd_mono)
 apply (assumption | rule quniv_mono basic_monos)+
@@ -184,7 +184,7 @@
 (*** lconst -- defined directly using lfp, but equivalent to a LList_corec ***)
 
 lemma lconst_fun_bnd_mono: "bnd_mono(univ(a), \<lambda>l. LCons(a,l))"
-apply (unfold llist.con_defs )
+  unfolding llist.con_defs 
 apply (rule bnd_monoI)
 apply (blast intro: A_subset_univ QInr_subset_univ)
 apply (blast intro: subset_refl QInr_mono QPair_mono)
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/ex/Ramsey.thy
--- a/src/ZF/ex/Ramsey.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/ex/Ramsey.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -79,7 +79,7 @@
 
 lemma Atleast_succI: 
     "\<lbrakk>Atleast(m,B);  b\<notin> B\<rbrakk> \<Longrightarrow> Atleast(succ(m), cons(b,B))"
-apply (unfold Atleast_def succ_def)
+  unfolding Atleast_def succ_def
 apply (blast intro: inj_extend elim: mem_irrefl) 
 done
 
@@ -148,7 +148,7 @@
     "\<lbrakk>Indept(I, {z \<in> V-{a}. \<langle>a,z\<rangle> \<notin> E}, E);  Symmetric(E);  a \<in> V;   
         Atleast(j,I)\<rbrakk> \<Longrightarrow>    
      Indept(cons(a,I), V, E) \<and> Atleast(succ(j), cons(a,I))"
-apply (unfold Symmetric_def Indept_def)
+  unfolding Symmetric_def Indept_def
 apply (blast intro!: Atleast_succI)
 done
 
@@ -157,7 +157,7 @@
     "\<lbrakk>Clique(C, {z \<in> V-{a}. \<langle>a,z\<rangle>:E}, E);  Symmetric(E);  a \<in> V;   
         Atleast(j,C)\<rbrakk> \<Longrightarrow>    
      Clique(cons(a,C), V, E) \<and> Atleast(succ(j), cons(a,C))"
-apply (unfold Symmetric_def Clique_def)
+  unfolding Symmetric_def Clique_def
 apply (blast intro!: Atleast_succI)
 done
 
diff -r 9fc34f76b4e8 -r 8655344f1cf6 src/ZF/func.thy
--- a/src/ZF/func.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/func.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -318,7 +318,7 @@
 by (simp add: restrict_def relation_def, blast)
 
 lemma domain_restrict_lam [simp]: "domain(restrict(Lambda(A,f),C)) = A \<inter> C"
-apply (unfold restrict_def lam_def)
+  unfolding restrict_def lam_def
 apply (rule equalityI)
 apply (auto simp add: domain_iff)
 done