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/SubstAx.thy
changeset 5277 e4297d03e5d2
parent 5253 82a5ca6290aa
child 5313 1861a564d7e2 
--- a/src/HOL/UNITY/SubstAx.thy	Thu Aug 06 14:04:49 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.thy	Thu Aug 06 15:47:26 1998 +0200
@@ -3,10 +3,10 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
-My treatment of the Substitution Axiom -- not as an axiom!
+LeadsTo relation: restricted to the set of reachable states.
 *)
 
-SubstAx = WFair +
+SubstAx = WFair + Traces + 
 
 constdefs
isabelle