diff -r 304a47739407 -r 04ce6bb14d85 src/HOL/Hoare_Parallel/RG_Hoare.thy
--- a/src/HOL/Hoare_Parallel/RG_Hoare.thy	Thu Sep 24 19:14:18 2009 +0200
+++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy	Fri Sep 25 09:50:31 2009 +0200
@@ -4,8 +4,8 @@
 
 subsection {* Proof System for Component Programs *}
 
-declare Un_subset_iff [iff del]
-declare Cons_eq_map_conv[iff]
+declare Un_subset_iff [simp del] le_sup_iff [simp del]
+declare Cons_eq_map_conv [iff]
 
 constdefs
   stable :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool"