# HG changeset patch
# User wenzelm
# Date 1178732239 -7200
# Node ID 619b270607ac098fd69277375c6e54efd72853f2
# Parent  1b0f4e6f81aa9ae2b02a47dd86f707d7e2a4c1a0
eliminated unnamed infixes;

diff -r 1b0f4e6f81aa -r 619b270607ac src/Sequents/ILL.thy
--- a/src/Sequents/ILL.thy	Wed May 09 19:37:18 2007 +0200
+++ b/src/Sequents/ILL.thy	Wed May 09 19:37:19 2007 +0200
@@ -11,16 +11,16 @@
 consts
   Trueprop       :: "two_seqi"
 
-"><"    ::"[o, o] => o"        (infixr 35)
-"-o"    ::"[o, o] => o"        (infixr 45)
-"o-o"   ::"[o, o] => o"        (infixr 45)
-FShriek ::"o => o"             ("! _" [100] 1000)
-"&&"    ::"[o, o] => o"        (infixr 35)
-"++"    ::"[o, o] => o"        (infixr 35)
-zero    ::"o"                  ("0")
-top     ::"o"                  ("1")
-eye     ::"o"                  ("I")
-aneg    ::"o=>o"               ("~_")
+  tens :: "[o, o] => o"        (infixr "><" 35)
+  limp :: "[o, o] => o"        (infixr "-o" 45)
+  liff :: "[o, o] => o"        (infixr "o-o" 45)
+  FShriek :: "o => o"          ("! _" [100] 1000)
+  lconj :: "[o, o] => o"       (infixr "&&" 35)
+  ldisj :: "[o, o] => o"       (infixr "++" 35)
+  zero :: "o"                  ("0")
+  top :: "o"                   ("1")
+  eye :: "o"                   ("I")
+  aneg :: "o=>o"               ("~_")
 
 
   (* context manipulation *)
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