--- a/src/HOL/UNITY/Simple/Reach.thy Wed May 07 10:59:39 2008 +0200
+++ b/src/HOL/UNITY/Simple/Reach.thy Wed May 07 10:59:40 2008 +0200
@@ -105,7 +105,8 @@
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 (auto simp add: Compl_FP UN_UN_flatten)
+apply (rule subset_antisym)
+apply (auto simp add: Compl_FP UN_UN_flatten del: subset_antisym)
apply (rule fun_upd_idem, force)
apply (force intro!: rev_bexI simp add: fun_upd_idem_iff)
done