eliminated unnamed infixes;
authorwenzelm
Wed May 09 19:37:19 2007 +0200 (2007-05-09)
changeset 22894619b270607ac
parent 22893 1b0f4e6f81aa
child 22895 adc529c89281
eliminated unnamed infixes;
src/Sequents/ILL.thy
src/Sequents/LK0.thy
     1.1 --- a/src/Sequents/ILL.thy	Wed May 09 19:37:18 2007 +0200
     1.2 +++ b/src/Sequents/ILL.thy	Wed May 09 19:37:19 2007 +0200
     1.3 @@ -11,16 +11,16 @@
     1.4  consts
     1.5    Trueprop       :: "two_seqi"
     1.6  
     1.7 -"><"    ::"[o, o] => o"        (infixr 35)
     1.8 -"-o"    ::"[o, o] => o"        (infixr 45)
     1.9 -"o-o"   ::"[o, o] => o"        (infixr 45)
    1.10 -FShriek ::"o => o"             ("! _" [100] 1000)
    1.11 -"&&"    ::"[o, o] => o"        (infixr 35)
    1.12 -"++"    ::"[o, o] => o"        (infixr 35)
    1.13 -zero    ::"o"                  ("0")
    1.14 -top     ::"o"                  ("1")
    1.15 -eye     ::"o"                  ("I")
    1.16 -aneg    ::"o=>o"               ("~_")
    1.17 +  tens :: "[o, o] => o"        (infixr "><" 35)
    1.18 +  limp :: "[o, o] => o"        (infixr "-o" 45)
    1.19 +  liff :: "[o, o] => o"        (infixr "o-o" 45)
    1.20 +  FShriek :: "o => o"          ("! _" [100] 1000)
    1.21 +  lconj :: "[o, o] => o"       (infixr "&&" 35)
    1.22 +  ldisj :: "[o, o] => o"       (infixr "++" 35)
    1.23 +  zero :: "o"                  ("0")
    1.24 +  top :: "o"                   ("1")
    1.25 +  eye :: "o"                   ("I")
    1.26 +  aneg :: "o=>o"               ("~_")
    1.27  
    1.28  
    1.29    (* context manipulation *)
     2.1 --- a/src/Sequents/LK0.thy	Wed May 09 19:37:18 2007 +0200
     2.2 +++ b/src/Sequents/LK0.thy	Wed May 09 19:37:19 2007 +0200
     2.3 @@ -24,43 +24,43 @@
     2.4  
     2.5    True         :: o
     2.6    False        :: o
     2.7 -  "="          :: "['a,'a] => o"     (infixl 50)
     2.8 +  equal        :: "['a,'a] => o"     (infixl "=" 50)
     2.9    Not          :: "o => o"           ("~ _" [40] 40)
    2.10 -  "&"          :: "[o,o] => o"       (infixr 35)
    2.11 -  "|"          :: "[o,o] => o"       (infixr 30)
    2.12 -  "-->"        :: "[o,o] => o"       (infixr 25)
    2.13 -  "<->"        :: "[o,o] => o"       (infixr 25)
    2.14 +  conj         :: "[o,o] => o"       (infixr "&" 35)
    2.15 +  disj         :: "[o,o] => o"       (infixr "|" 30)
    2.16 +  imp          :: "[o,o] => o"       (infixr "-->" 25)
    2.17 +  iff          :: "[o,o] => o"       (infixr "<->" 25)
    2.18    The          :: "('a => o) => 'a"  (binder "THE " 10)
    2.19    All          :: "('a => o) => o"   (binder "ALL " 10)
    2.20    Ex           :: "('a => o) => o"   (binder "EX " 10)
    2.21  
    2.22  syntax
    2.23   "@Trueprop"    :: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
    2.24 -  "_not_equal" :: "['a, 'a] => o"              (infixl "~=" 50)
    2.25  
    2.26  parse_translation {* [("@Trueprop", two_seq_tr "Trueprop")] *}
    2.27  print_translation {* [("Trueprop", two_seq_tr' "@Trueprop")] *}
    2.28  
    2.29 -translations
    2.30 -  "x ~= y"      == "~ (x = y)"
    2.31 +abbreviation
    2.32 +  not_equal  (infixl "~=" 50) where
    2.33 +  "x ~= y == ~ (x = y)"
    2.34  
    2.35  syntax (xsymbols)
    2.36    Not           :: "o => o"               ("\<not> _" [40] 40)
    2.37 -  "op &"        :: "[o, o] => o"          (infixr "\<and>" 35)
    2.38 -  "op |"        :: "[o, o] => o"          (infixr "\<or>" 30)
    2.39 -  "op -->"      :: "[o, o] => o"          (infixr "\<longrightarrow>" 25)
    2.40 -  "op <->"      :: "[o, o] => o"          (infixr "\<longleftrightarrow>" 25)
    2.41 +  conj          :: "[o, o] => o"          (infixr "\<and>" 35)
    2.42 +  disj          :: "[o, o] => o"          (infixr "\<or>" 30)
    2.43 +  imp           :: "[o, o] => o"          (infixr "\<longrightarrow>" 25)
    2.44 +  iff           :: "[o, o] => o"          (infixr "\<longleftrightarrow>" 25)
    2.45    All_binder    :: "[idts, o] => o"       ("(3\<forall>_./ _)" [0, 10] 10)
    2.46    Ex_binder     :: "[idts, o] => o"       ("(3\<exists>_./ _)" [0, 10] 10)
    2.47 -  "_not_equal"  :: "['a, 'a] => o"        (infixl "\<noteq>" 50)
    2.48 +  not_equal     :: "['a, 'a] => o"        (infixl "\<noteq>" 50)
    2.49  
    2.50  syntax (HTML output)
    2.51    Not           :: "o => o"               ("\<not> _" [40] 40)
    2.52 -  "op &"        :: "[o, o] => o"          (infixr "\<and>" 35)
    2.53 -  "op |"        :: "[o, o] => o"          (infixr "\<or>" 30)
    2.54 +  conj          :: "[o, o] => o"          (infixr "\<and>" 35)
    2.55 +  disj          :: "[o, o] => o"          (infixr "\<or>" 30)
    2.56    All_binder    :: "[idts, o] => o"       ("(3\<forall>_./ _)" [0, 10] 10)
    2.57    Ex_binder     :: "[idts, o] => o"       ("(3\<exists>_./ _)" [0, 10] 10)
    2.58 -  "_not_equal"  :: "['a, 'a] => o"        (infixl "\<noteq>" 50)
    2.59 +  not_equal     :: "['a, 'a] => o"        (infixl "\<noteq>" 50)
    2.60  
    2.61  local
    2.62