diff -r 649b98cf9bc3 -r 9dd06eeda95c src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Fri Dec 11 17:16:23 1998 +0100
+++ b/src/FOL/IFOL.thy	Fri Dec 11 18:56:30 1998 +0100
@@ -63,6 +63,9 @@
   "EX! "        :: [idts, o] => o               ("(3\\<exists>!_./ _)" [0, 10] 10)
   "op ~="       :: ['a, 'a] => o                (infixl "\\<noteq>" 50)
 
+syntax (xsymbols)
+  "op -->"      :: [o, o] => o                  (infixr "\\<longrightarrow>" 25)
+  "op <->"      :: [o, o] => o                  (infixr "\\<longleftrightarrow>" 25)
 
 local