src/Sequents/LK0.thy
changeset 12116 4027b15377a5
parent 7166 a4a870ec2e67
child 12662 a9bbba3473f3
--- a/src/Sequents/LK0.thy	Fri Nov 09 00:11:52 2001 +0100
+++ b/src/Sequents/LK0.thy	Fri Nov 09 00:14:17 2001 +0100
@@ -40,21 +40,17 @@
 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)
+  "op -->"      :: [o, o] => o          (infixr "\\<longrightarrow>" 25)
+  "op <->"      :: [o, o] => o          (infixr "\\<longleftrightarrow>" 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)
-
 syntax (HTML output)
   Not           :: o => o               ("\\<not> _" [40] 40)