diff -r e9326ab92fbc -r c8154379738c src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Wed Nov 27 16:41:56 1996 +0100
+++ b/src/FOL/IFOL.thy	Wed Nov 27 16:42:48 1996 +0100
@@ -43,22 +43,23 @@
   Ex1           :: ('a => o) => o               (binder "EX! " 10)
 
 
+
 syntax
   "~="          :: ['a, 'a] => o                (infixl 50)
 
 translations
   "x ~= y"      == "~ (x = y)"
 
-syntax (symbolfont)
-  Not           :: o => o                       ("\\{neg} _" [40] 40)
-  "op &"        :: [o, o] => o                  (infixr "\\{vee}" 35)
-  "op |"        :: [o, o] => o                  (infixr "\\{wedge}" 30)
-  "op -->"      :: [o, o] => o                  (infixr "\\{midarrow}\\{rightarrow}" 25)
-  "op <->"      :: [o, o] => o                  (infixr "\\{leftarrow}\\{rightarrow}" 25)
-  "ALL "        :: [idts, o] => o               ("(3\\{forall}_./ _)" 10)
-  "EX "         :: [idts, o] => o               ("(3\\{exists}_./ _)" 10)
-  "EX! "        :: [idts, o] => o               ("(3\\{exists}!_./ _)" 10)
-  "op ~="       :: ['a, 'a] => o                (infixl "\\{noteq}" 50)
+syntax (symbols)
+  Not           :: o => o                       ("\\<not> _" [40] 40)
+  "op &"        :: [o, o] => o                  (infixr "\\<and>" 35)
+  "op |"        :: [o, o] => o                  (infixr "\\<or>" 30)
+  "op -->"      :: [o, o] => o                  (infixr "\\<midarrow>\\<rightarrow>" 25)
+  "op <->"      :: [o, o] => o                  (infixr "\\<leftarrow>\\<rightarrow>" 25)
+  "ALL "        :: [idts, o] => o               ("(3\\<forall>_./ _)" 10)
+  "EX "         :: [idts, o] => o               ("(3\\<exists>_./ _)" 10)
+  "EX! "        :: [idts, o] => o               ("(3\\<exists>!_./ _)" 10)
+  "op ~="       :: ['a, 'a] => o                (infixl "\\<noteq>" 50)
 
 
 rules