src/HOL/UNITY/SubstAx.thy

--- a/src/HOL/UNITY/SubstAx.thy	Tue Nov 30 16:51:41 1999 +0100
+++ b/src/HOL/UNITY/SubstAx.thy	Tue Nov 30 16:54:10 1999 +0100
@@ -8,10 +8,8 @@
 
 SubstAx = WFair + Constrains + 
 
-consts
-   LeadsTo :: "['a set, 'a set] => 'a program set"       (infixl 60)
+constdefs
+   LeadsTo :: "['a set, 'a set] => 'a program set"            (infixl 60)
+    "A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}"
 
-defs
-   LeadsTo_def
-    "A LeadsTo B == {F. F : (reachable F Int A) leadsTo  B}"
 end