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