src/HOL/UNITY/SubstAx.thy
changeset 6536 281d44905cab
parent 5648 fe887910e32e
child 6575 70d758762c50
--- a/src/HOL/UNITY/SubstAx.thy	Wed Apr 28 13:36:31 1999 +0200
+++ b/src/HOL/UNITY/SubstAx.thy	Thu Apr 29 10:51:58 1999 +0200
@@ -3,14 +3,16 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
-LeadsTo relation: restricted to the set of reachable states.
+Weak LeadsTo relation (restricted to the set of reachable states)
 *)
 
 SubstAx = WFair + Constrains + 
 
-constdefs
+consts
+   LeadsTo :: "['a set, 'a set] => 'a program set"       (infixl 60)
 
-   LeadsTo :: "['a set, 'a set] => 'a program set"
-    "LeadsTo A B == {F. F : leadsTo (reachable F  Int  A)
-	   	                    (reachable F  Int  B)}"
+defs
+   LeadsTo_def
+    "A LeadsTo B == {F. F : (reachable F  Int  A) leadsTo
+	   	            (reachable F  Int  B)}"
 end