--- a/src/HOL/HoareParallel/Gar_Coll.thy Tue Dec 05 22:14:53 2006 +0100
+++ b/src/HOL/HoareParallel/Gar_Coll.thy Wed Dec 06 01:12:36 2006 +0100
@@ -798,7 +798,7 @@
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 psubset_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 ())]) *})
done
subsubsection {* Interference freedom Mutator-Collector *}