--- a/src/HOL/HoareParallel/Gar_Coll.thy Sat Jul 08 12:54:37 2006 +0200
+++ b/src/HOL/HoareParallel/Gar_Coll.thy Sat Jul 08 12:54:38 2006 +0200
@@ -796,9 +796,9 @@
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
apply(tactic {* TRYALL (etac disjE) *})
apply simp_all
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac (thm "Graph3"),Force_tac, assume_tac]) *})
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac (thm "Graph9"),Force_tac]) *})
-apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac psubset_subset_trans,rtac (thm "Graph9"),Force_tac]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac (thm "Graph3"),force_tac (clasimpset ()), assume_tac]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac (thm "Graph9"),force_tac (clasimpset ())]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac psubset_subset_trans,rtac (thm "Graph9"),force_tac (clasimpset ())]) *})
done
subsubsection {* Interference freedom Mutator-Collector *}