tuned proofs; be more cautios wrt. default simp rules

--- a/src/HOL/Hoare_Parallel/Gar_Coll.thy	Mon Sep 21 11:01:49 2009 +0200
+++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy	Mon Sep 21 12:23:52 2009 +0200
@@ -253,7 +253,7 @@
     \<and> ( \<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)}."
 apply (unfold Propagate_Black_def  PBInv_def Auxk_def collector_defs)
 apply annhoare
-apply(simp_all add:Graph6 Graph7 Graph8 Graph12)
+apply(simp_all add: Graph6 Graph7 Graph8 Graph12)
        apply force
       apply force
      apply force
@@ -297,8 +297,6 @@
 apply(erule subset_psubset_trans)
 apply(erule Graph11)
 apply fast
---{* 3 subgoals left *}
-apply force
 --{* 2 subgoals left *}
 apply clarify
 apply(simp add:Proper_Edges_def Graph6 Graph7 Graph8 Graph12)

--- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Mon Sep 21 11:01:49 2009 +0200
+++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Mon Sep 21 12:23:52 2009 +0200
@@ -276,8 +276,6 @@
   apply(force)
  apply(force)
 apply(rule disjI2, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
---{* 3 subgoals left *}
-apply force
 --{* 2 subgoals left *}
 apply clarify
 apply(conjI_tac)
@@ -1235,9 +1233,9 @@
 apply(unfold mul_modules mul_collector_defs mul_mutator_defs)
 apply(tactic  {* TRYALL (interfree_aux_tac) *})
 --{* 76 subgoals left *}
-apply (clarify,simp add: nth_list_update)+
+apply (clarsimp simp add: nth_list_update)+
 --{* 56 subgoals left *}
-apply(clarify,simp add:Mul_AppendInv_def Append_to_free0 nth_list_update)+
+apply (clarsimp simp add: Mul_AppendInv_def Append_to_free0 nth_list_update)+
 done
 
 subsubsection {* The Multi-Mutator Garbage Collection Algorithm *}

--- a/src/HOL/Hoare_Parallel/RG_Hoare.thy	Mon Sep 21 11:01:49 2009 +0200
+++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy	Mon Sep 21 12:23:52 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"