src/HOL/UNITY/SubstAx.thy
changeset 5111 8f4b72f0c15d
parent 4776 1f9362e769c1
child 5253 82a5ca6290aa
     1.1 --- a/src/HOL/UNITY/SubstAx.thy	Thu Jul 02 16:44:39 1998 +0200
     1.2 +++ b/src/HOL/UNITY/SubstAx.thy	Thu Jul 02 16:53:55 1998 +0200
     1.3 @@ -10,10 +10,10 @@
     1.4  
     1.5  constdefs
     1.6  
     1.7 -   LeadsTo :: "['a set, ('a * 'a)set set, 'a set, 'a set] => bool"
     1.8 -    "LeadsTo Init Acts A B ==
     1.9 -     leadsTo Acts (reachable Init Acts Int A)
    1.10 -                  (reachable Init Acts Int B)"
    1.11 +   LeadsTo :: "['a set * ('a * 'a)set set, 'a set, 'a set] => bool"
    1.12 +    "LeadsTo == %(Init,Acts) A B.
    1.13 +		 leadsTo Acts (reachable (Init,Acts) Int A)
    1.14 +			      (reachable (Init,Acts) Int B)"
    1.15  
    1.16  
    1.17  end