src/HOL/UNITY/SubstAx.thy

--- a/src/HOL/UNITY/SubstAx.thy	Thu Aug 24 11:14:21 2000 +0200
+++ b/src/HOL/UNITY/SubstAx.thy	Thu Aug 24 12:39:24 2000 +0200
@@ -15,4 +15,7 @@
    LeadsTo :: "['a set, 'a set] => 'a program set"            (infixl 60)
     "A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}"
 
+syntax (xsymbols)
+  "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \\<longmapsto>w " 60)
+
 end