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