# HG changeset patch
# User berghofe
# Date 1210150781 -7200
# Node ID fd8fdf21660f49235f0e40b4b2b5fac61fce44c2
# Parent  0373ed6f04b139978a02e42ff08f37e94cd772e8
- Tuned imports
- Replaced blast by simp in proof of Stable_final_E_NOT_empty, since blast looped
  because of the new encoding of sets.

diff -r 0373ed6f04b1 -r fd8fdf21660f src/HOL/UNITY/Simple/Reachability.thy
--- 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])