--- 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)