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