src/HOL/UNITY/SubstAx.thy
changeset 5648 fe887910e32e
parent 5620 3ac11c4af76a
child 6536 281d44905cab
     1.1 --- a/src/HOL/UNITY/SubstAx.thy	Wed Oct 14 15:47:22 1998 +0200
     1.2 +++ b/src/HOL/UNITY/SubstAx.thy	Thu Oct 15 11:35:07 1998 +0200
     1.3 @@ -10,9 +10,7 @@
     1.4  
     1.5  constdefs
     1.6  
     1.7 -   LeadsTo :: "['a program, 'a set, 'a set] => bool"
     1.8 -    "LeadsTo F A B ==
     1.9 -		 leadsTo (Acts F)
    1.10 -                         (reachable F  Int  A)
    1.11 -  		         (reachable F  Int  B)"
    1.12 +   LeadsTo :: "['a set, 'a set] => 'a program set"
    1.13 +    "LeadsTo A B == {F. F : leadsTo (reachable F  Int  A)
    1.14 +	   	                    (reachable F  Int  B)}"
    1.15  end