--- a/src/HOL/Hoare_Parallel/Gar_Coll.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy Fri May 13 22:55:00 2011 +0200
@@ -774,13 +774,13 @@
--{* 32 subgoals left *}
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
--{* 20 subgoals left *}
-apply(tactic{* TRYALL (clarify_tac @{claset}) *})
+apply(tactic{* TRYALL (clarify_tac @{context}) *})
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 @{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 @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{clasimpset}]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac @{thm Graph9},force_tac @{context}]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}]) *})
done
subsubsection {* Interference freedom Mutator-Collector *}
@@ -794,7 +794,7 @@
apply(tactic {* TRYALL (interfree_aux_tac) *})
--{* 64 subgoals left *}
apply(simp_all add:nth_list_update Invariants Append_to_free0)+
-apply(tactic{* TRYALL (clarify_tac @{claset}) *})
+apply(tactic{* TRYALL (clarify_tac @{context}) *})
--{* 4 subgoals left *}
apply force
apply(simp add:Append_to_free2)