src/HOL/HoareParallel/RG_Hoare.thy

--- a/src/HOL/HoareParallel/RG_Hoare.thy	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/HoareParallel/RG_Hoare.thy	Wed Dec 21 12:02:57 2005 +0100
@@ -5,6 +5,8 @@
 subsection {* Proof System for Component Programs *}
 
 declare Un_subset_iff [iff del]
+declare not_None_eq [iff]
+declare Cons_eq_map_conv[iff]
 
 constdefs
   stable :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool"