--- 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