diff -r 1b0f4e6f81aa -r 619b270607ac src/Sequents/LK0.thy
--- a/src/Sequents/LK0.thy	Wed May 09 19:37:18 2007 +0200
+++ b/src/Sequents/LK0.thy	Wed May 09 19:37:19 2007 +0200
@@ -24,43 +24,43 @@
 
   True         :: o
   False        :: o
-  "="          :: "['a,'a] => o"     (infixl 50)
+  equal        :: "['a,'a] => o"     (infixl "=" 50)
   Not          :: "o => o"           ("~ _" [40] 40)
-  "&"          :: "[o,o] => o"       (infixr 35)
-  "|"          :: "[o,o] => o"       (infixr 30)
-  "-->"        :: "[o,o] => o"       (infixr 25)
-  "<->"        :: "[o,o] => o"       (infixr 25)
+  conj         :: "[o,o] => o"       (infixr "&" 35)
+  disj         :: "[o,o] => o"       (infixr "|" 30)
+  imp          :: "[o,o] => o"       (infixr "-->" 25)
+  iff          :: "[o,o] => o"       (infixr "<->" 25)
   The          :: "('a => o) => 'a"  (binder "THE " 10)
   All          :: "('a => o) => o"   (binder "ALL " 10)
   Ex           :: "('a => o) => o"   (binder "EX " 10)
 
 syntax
  "@Trueprop"    :: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
-  "_not_equal" :: "['a, 'a] => o"              (infixl "~=" 50)
 
 parse_translation {* [("@Trueprop", two_seq_tr "Trueprop")] *}
 print_translation {* [("Trueprop", two_seq_tr' "@Trueprop")] *}
 
-translations
-  "x ~= y"      == "~ (x = y)"
+abbreviation
+  not_equal  (infixl "~=" 50) where
+  "x ~= y == ~ (x = y)"
 
 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 "\<longrightarrow>" 25)
-  "op <->"      :: "[o, o] => o"          (infixr "\<longleftrightarrow>" 25)
+  conj          :: "[o, o] => o"          (infixr "\<and>" 35)
+  disj          :: "[o, o] => o"          (infixr "\<or>" 30)
+  imp           :: "[o, o] => o"          (infixr "\<longrightarrow>" 25)
+  iff           :: "[o, o] => o"          (infixr "\<longleftrightarrow>" 25)
   All_binder    :: "[idts, o] => o"       ("(3\<forall>_./ _)" [0, 10] 10)
   Ex_binder     :: "[idts, o] => o"       ("(3\<exists>_./ _)" [0, 10] 10)
-  "_not_equal"  :: "['a, 'a] => o"        (infixl "\<noteq>" 50)
+  not_equal     :: "['a, 'a] => o"        (infixl "\<noteq>" 50)
 
 syntax (HTML output)
   Not           :: "o => o"               ("\<not> _" [40] 40)
-  "op &"        :: "[o, o] => o"          (infixr "\<and>" 35)
-  "op |"        :: "[o, o] => o"          (infixr "\<or>" 30)
+  conj          :: "[o, o] => o"          (infixr "\<and>" 35)
+  disj          :: "[o, o] => o"          (infixr "\<or>" 30)
   All_binder    :: "[idts, o] => o"       ("(3\<forall>_./ _)" [0, 10] 10)
   Ex_binder     :: "[idts, o] => o"       ("(3\<exists>_./ _)" [0, 10] 10)
-  "_not_equal"  :: "['a, 'a] => o"        (infixl "\<noteq>" 50)
+  not_equal     :: "['a, 'a] => o"        (infixl "\<noteq>" 50)
 
 local