src/FOL/IFOL.thy
changeset 12114 a8e860c86252
parent 12019 abe9b7c6016e
child 12349 94e812f9683e
--- a/src/FOL/IFOL.thy	Fri Nov 09 00:06:15 2001 +0100
+++ b/src/FOL/IFOL.thy	Fri Nov 09 00:09:47 2001 +0100
@@ -47,18 +47,14 @@
 translations
   "x ~= y"      == "~ (x = y)"
 
-syntax (symbols)
+syntax (xsymbols)
   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>_./ _)" [0, 10] 10)
   "EX "         :: "[idts, o] => o"             ("(3\<exists>_./ _)" [0, 10] 10)
   "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)