--- a/src/HOL/UNITY/Simple/Reach.thy Wed Dec 28 15:08:12 2011 +0100
+++ b/src/HOL/UNITY/Simple/Reach.thy Wed Dec 28 20:03:13 2011 +0100
@@ -103,7 +103,7 @@
lemma Compl_fixedpoint: "- fixedpoint = (\<Union>(u,v)\<in>edges. {s. s u & ~ s v})"
apply (simp add: FP_fixedpoint [symmetric] Rprg_def mk_total_program_def)
apply (rule subset_antisym)
-apply (auto simp add: Compl_FP UN_UN_flatten del: subset_antisym)
+apply (auto simp add: Compl_FP UN_UN_flatten)
apply (rule fun_upd_idem, force)
apply (force intro!: rev_bexI simp add: fun_upd_idem_iff)
done