--- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Mon Sep 06 19:13:10 2010 +0200
@@ -1199,15 +1199,15 @@
apply(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 (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *})
+apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans}, etac @{thm Graph11},force_tac @{clasimpset}]) *})
--{* 41 subgoals left *}
apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (@{claset},@{simpset} addsimps [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}])]) *})
--{* 35 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "psubset_subset_trans"),rtac (thm "Graph9"),force_tac @{clasimpset}]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{clasimpset}]) *})
--{* 31 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{clasimpset}]) *})
--{* 29 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *})
+apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans},etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{clasimpset}]) *})
--{* 25 subgoals left *}
apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (@{claset},@{simpset} addsimps [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}])]) *})
--{* 10 subgoals left *}