src/HOL/UNITY/SubstAx.thy
changeset 8041 e3237d8c18d6
parent 6575 70d758762c50
child 8122 b43ad07660b9
     1.1 --- a/src/HOL/UNITY/SubstAx.thy	Tue Nov 30 16:51:41 1999 +0100
     1.2 +++ b/src/HOL/UNITY/SubstAx.thy	Tue Nov 30 16:54:10 1999 +0100
     1.3 @@ -8,10 +8,8 @@
     1.4  
     1.5  SubstAx = WFair + Constrains + 
     1.6  
     1.7 -consts
     1.8 -   LeadsTo :: "['a set, 'a set] => 'a program set"       (infixl 60)
     1.9 +constdefs
    1.10 +   LeadsTo :: "['a set, 'a set] => 'a program set"            (infixl 60)
    1.11 +    "A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}"
    1.12  
    1.13 -defs
    1.14 -   LeadsTo_def
    1.15 -    "A LeadsTo B == {F. F : (reachable F Int A) leadsTo  B}"
    1.16  end