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