src/HOL/UNITY/SubstAx.thy
changeset 5277 e4297d03e5d2
parent 5253 82a5ca6290aa
child 5313 1861a564d7e2
     1.1 --- a/src/HOL/UNITY/SubstAx.thy	Thu Aug 06 14:04:49 1998 +0200
     1.2 +++ b/src/HOL/UNITY/SubstAx.thy	Thu Aug 06 15:47:26 1998 +0200
     1.3 @@ -3,10 +3,10 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1998  University of Cambridge
     1.6  
     1.7 -My treatment of the Substitution Axiom -- not as an axiom!
     1.8 +LeadsTo relation: restricted to the set of reachable states.
     1.9  *)
    1.10  
    1.11 -SubstAx = WFair +
    1.12 +SubstAx = WFair + Traces + 
    1.13  
    1.14  constdefs
    1.15