Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
- Tuned imports
authorberghofe
Wed, 07 May 2008 10:59:41 +0200
changeset 26826 fd8fdf21660f
parent 26825 0373ed6f04b1
child 26827 a62f8db42f4a
- Tuned imports - Replaced blast by simp in proof of Stable_final_E_NOT_empty, since blast looped because of the new encoding of sets.
src/HOL/UNITY/Simple/Reachability.thy file | annotate | diff | comparison | revisions 
--- 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])
isabelle