# HG changeset patch
# User wenzelm
# Date 1152356078 -7200
# Node ID a2fb9d553aadf17ad34736ab1561e07388fab749
# Parent  f48c4a3a34bc3ac394b37c62453048232c6ff2dd
avoid Force_tac, which uses a different context;

diff -r f48c4a3a34bc -r a2fb9d553aad src/HOL/HoareParallel/Gar_Coll.thy
--- 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 *}
diff -r f48c4a3a34bc -r a2fb9d553aad src/HOL/HoareParallel/Mul_Gar_Coll.thy
--- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Sat Jul 08 12:54:37 2006 +0200
+++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Sat Jul 08 12:54:38 2006 +0200
@@ -1201,7 +1201,7 @@
 --{* 72 subgoals left *}
 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
 --{* 35 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac (thm "Graph3"),Force_tac, assume_tac]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac (thm "Graph3"),force_tac (clasimpset ()), assume_tac]) *})
 --{* 28 subgoals left *}
 apply(tactic {* TRYALL (etac conjE) *})
 apply(tactic {* TRYALL (etac disjE) *})
@@ -1211,15 +1211,15 @@
 apply(tactic {* ALLGOALS(case_tac "M x!(T (Muts x ! j))=Black") *})
 apply(simp_all add:Graph10)
 --{* 47 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac subset_psubset_trans,etac (thm "Graph11"),Force_tac]) *})
+apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac subset_psubset_trans,etac (thm "Graph11"),force_tac (clasimpset ())]) *})
 --{* 41 subgoals left *}
 apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac le_trans, force_tac (claset(),simpset() addsimps [thm "Queue_def", less_Suc_eq_le, thm "le_length_filter_update"])]) *})
 --{* 35 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac psubset_subset_trans,rtac (thm "Graph9"),Force_tac]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac psubset_subset_trans,rtac (thm "Graph9"),force_tac (clasimpset ())]) *})
 --{* 31 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac subset_psubset_trans,etac (thm "Graph11"),Force_tac]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac subset_psubset_trans,etac (thm "Graph11"),force_tac (clasimpset ())]) *})
 --{* 29 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac subset_psubset_trans,etac subset_psubset_trans,etac (thm "Graph11"),Force_tac]) *})
+apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac subset_psubset_trans,etac subset_psubset_trans,etac (thm "Graph11"),force_tac (clasimpset ())]) *})
 --{* 25 subgoals left *}
 apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac le_trans, force_tac (claset(),simpset() addsimps [thm "Queue_def", less_Suc_eq_le, thm "le_length_filter_update"])]) *})
 --{* 10 subgoals left *}