--- a/src/HOL/Hoare_Parallel/RG_Hoare.thy Wed Dec 25 10:09:43 2013 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy Wed Dec 25 15:52:25 2013 +0100
@@ -4,7 +4,7 @@
subsection {* Proof System for Component Programs *}
-declare Un_subset_iff [simp del] le_sup_iff [simp del]
+declare Un_subset_iff [simp del] sup.bounded_iff [simp del]
definition stable :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" where
"stable \<equiv> \<lambda>f g. (\<forall>x y. x \<in> f \<longrightarrow> (x, y) \<in> g \<longrightarrow> y \<in> f)"