--- a/src/HOL/UNITY/Simple/Reachability.thy Wed May 07 10:59:40 2008 +0200
+++ b/src/HOL/UNITY/Simple/Reachability.thy Wed May 07 10:59:41 2008 +0200
@@ -8,7 +8,7 @@
From Chandy and Misra, "Parallel Program Design" (1989), sections 6.2 and 11.3
*)
-theory Reachability imports Detects Reach begin
+theory Reachability imports "../Detects" Reach begin
types edge = "(vertex*vertex)"
@@ -346,7 +346,7 @@
apply (subgoal_tac [2]
"({s. (s \<in> reachable v) = ((root,v) \<in> REACHABLE) } \<inter> nmsg_eq 0 (v,w)) =
({s. (s \<in> reachable v) = ( (root,v) \<in> REACHABLE) } \<inter> (- UNIV \<union> nmsg_eq 0 (v,w)))")
-prefer 2 apply blast
+prefer 2 apply simp
prefer 2 apply blast
apply (rule Stable_reachable_EQ_R_AND_nmsg_0
[simplified Eq_lemma2 Collect_const])