src/HOL/UNITY/SubstAx.thy
changeset 5620 3ac11c4af76a
parent 5313 1861a564d7e2
child 5648 fe887910e32e
     1.1 --- a/src/HOL/UNITY/SubstAx.thy	Wed Oct 07 10:31:30 1998 +0200
     1.2 +++ b/src/HOL/UNITY/SubstAx.thy	Wed Oct 07 10:32:00 1998 +0200
     1.3 @@ -11,8 +11,8 @@
     1.4  constdefs
     1.5  
     1.6     LeadsTo :: "['a program, 'a set, 'a set] => bool"
     1.7 -    "LeadsTo prg A B ==
     1.8 -		 leadsTo (Acts prg)
     1.9 -                         (reachable prg  Int  A)
    1.10 -  		         (reachable prg  Int  B)"
    1.11 +    "LeadsTo F A B ==
    1.12 +		 leadsTo (Acts F)
    1.13 +                         (reachable F  Int  A)
    1.14 +  		         (reachable F  Int  B)"
    1.15  end