src/Sequents/ILL.thy
changeset 22894 619b270607ac
parent 21588 cd0dc678a205
child 30510 4120fc59dd85
     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 *)