Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/UNITY/Simple/Reachability.thy
changeset 11701 3d51fbf81c17
parent 11467 1064effe37f6
child 13785 e2fcd88be55d 
--- a/src/HOL/UNITY/Simple/Reachability.thy	Fri Oct 05 21:50:37 2001 +0200
+++ b/src/HOL/UNITY/Simple/Reachability.thy	Fri Oct 05 21:52:39 2001 +0200
@@ -60,7 +60,7 @@
 
     MA4  "[|(v,w) : E|] ==> F : Always (-(reachable v) Un (nmsg_gt 0 (v,w)) Un (reachable w))"
 
-    MA5  "[|v:V;w:V|] ==> F : Always (nmsg_gte 0 (v,w) Int nmsg_lte 1' (v,w))"
+    MA5  "[|v:V;w:V|] ==> F : Always (nmsg_gte 0 (v,w) Int nmsg_lte (Suc 0) (v,w))"
 
     MA6  "[|v:V|] ==> F : Stable (reachable v)"
isabelle