src/HOL/UNITY/SubstAx.thy
changeset 6536 281d44905cab
parent 5648 fe887910e32e
child 6575 70d758762c50
     1.1 --- a/src/HOL/UNITY/SubstAx.thy	Wed Apr 28 13:36:31 1999 +0200
     1.2 +++ b/src/HOL/UNITY/SubstAx.thy	Thu Apr 29 10:51:58 1999 +0200
     1.3 @@ -3,14 +3,16 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1998  University of Cambridge
     1.6  
     1.7 -LeadsTo relation: restricted to the set of reachable states.
     1.8 +Weak LeadsTo relation (restricted to the set of reachable states)
     1.9  *)
    1.10  
    1.11  SubstAx = WFair + Constrains + 
    1.12  
    1.13 -constdefs
    1.14 +consts
    1.15 +   LeadsTo :: "['a set, 'a set] => 'a program set"       (infixl 60)
    1.16  
    1.17 -   LeadsTo :: "['a set, 'a set] => 'a program set"
    1.18 -    "LeadsTo A B == {F. F : leadsTo (reachable F  Int  A)
    1.19 -	   	                    (reachable F  Int  B)}"
    1.20 +defs
    1.21 +   LeadsTo_def
    1.22 +    "A LeadsTo B == {F. F : (reachable F  Int  A) leadsTo
    1.23 +	   	            (reachable F  Int  B)}"
    1.24  end