src/HOL/UNITY/SubstAx.thy

--- a/src/HOL/UNITY/SubstAx.thy	Tue May 04 13:32:53 1999 +0200
+++ b/src/HOL/UNITY/SubstAx.thy	Tue May 04 13:47:28 1999 +0200
@@ -13,6 +13,5 @@
 
 defs
    LeadsTo_def
-    "A LeadsTo B == {F. F : (reachable F  Int  A) leadsTo
-	   	            (reachable F  Int  B)}"
+    "A LeadsTo B == {F. F : (reachable F Int A) leadsTo  B}"
 end