--- a/src/HOL/Hoare_Parallel/Gar_Coll.thy Thu Jul 11 14:42:11 2013 +0200
+++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy Thu Jul 11 14:56:58 2013 +0200
@@ -75,7 +75,7 @@
apply(unfold Mutator_def)
apply annhoare
apply(simp_all add:Redirect_Edge Color_Target)
-apply(simp add:mutator_defs Redirect_Edge_def)
+apply(simp add:mutator_defs)
done
subsection {* The Collector *}
@@ -768,7 +768,7 @@
apply(unfold Collector_def Mutator_def)
apply interfree_aux
apply(simp_all add:collector_mutator_interfree)
-apply(unfold modules collector_defs mutator_defs)
+apply(unfold modules collector_defs Mut_init_def)
apply(tactic {* TRYALL (interfree_aux_tac @{context}) *})
--{* 32 subgoals left *}
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
@@ -789,7 +789,7 @@
apply(unfold Collector_def Mutator_def)
apply interfree_aux
apply(simp_all add:collector_mutator_interfree)
-apply(unfold modules collector_defs mutator_defs)
+apply(unfold modules collector_defs Mut_init_def)
apply(tactic {* TRYALL (interfree_aux_tac @{context}) *})
--{* 64 subgoals left *}
apply(simp_all add:nth_list_update Invariants Append_to_free0)+