src/HOL/UNITY/SubstAx.thy
changeset 8041 e3237d8c18d6
parent 6575 70d758762c50
child 8122 b43ad07660b9
--- 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