src/HOL/UNITY/SubstAx.thy
changeset 5111 8f4b72f0c15d
parent 4776 1f9362e769c1
child 5253 82a5ca6290aa
--- a/src/HOL/UNITY/SubstAx.thy	Thu Jul 02 16:44:39 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.thy	Thu Jul 02 16:53:55 1998 +0200
@@ -10,10 +10,10 @@
 
 constdefs
 
-   LeadsTo :: "['a set, ('a * 'a)set set, 'a set, 'a set] => bool"
-    "LeadsTo Init Acts A B ==
-     leadsTo Acts (reachable Init Acts Int A)
-                  (reachable Init Acts Int B)"
+   LeadsTo :: "['a set * ('a * 'a)set set, 'a set, 'a set] => bool"
+    "LeadsTo == %(Init,Acts) A B.
+		 leadsTo Acts (reachable (Init,Acts) Int A)
+			      (reachable (Init,Acts) Int B)"
 
 
 end