1.1 --- a/src/FOL/IFOL.thy	Fri Nov 09 00:06:15 2001 +0100
     1.2 +++ b/src/FOL/IFOL.thy	Fri Nov 09 00:09:47 2001 +0100
     1.3 @@ -47,18 +47,14 @@
     1.4  translations
     1.5    "x ~= y"      == "~ (x = y)"
     1.6  
     1.7 -syntax (symbols)
     1.8 +syntax (xsymbols)
     1.9    Not           :: "o => o"                     ("\<not> _" [40] 40)
    1.10    "op &"        :: "[o, o] => o"                (infixr "\<and>" 35)
    1.11    "op |"        :: "[o, o] => o"                (infixr "\<or>" 30)
    1.12 -  "op -->"      :: "[o, o] => o"                (infixr "\<midarrow>\<rightarrow>" 25)
    1.13 -  "op <->"      :: "[o, o] => o"                (infixr "\<leftarrow>\<rightarrow>" 25)
    1.14    "ALL "        :: "[idts, o] => o"             ("(3\<forall>_./ _)" [0, 10] 10)
    1.15    "EX "         :: "[idts, o] => o"             ("(3\<exists>_./ _)" [0, 10] 10)
    1.16    "EX! "        :: "[idts, o] => o"             ("(3\<exists>!_./ _)" [0, 10] 10)
    1.17    "op ~="       :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
    1.18 -
    1.19 -syntax (xsymbols)
    1.20    "op -->"      :: "[o, o] => o"                (infixr "\<longrightarrow>" 25)
    1.21    "op <->"      :: "[o, o] => o"                (infixr "\<longleftrightarrow>" 25)
    1.22