src/Sequents/ILL.thy
changeset 22894 619b270607ac
parent 21588 cd0dc678a205
child 30510 4120fc59dd85
equal deleted inserted replaced
22893:1b0f4e6f81aa 22894:619b270607ac
     9 begin
     9 begin
    10 
    10 
    11 consts
    11 consts
    12   Trueprop       :: "two_seqi"
    12   Trueprop       :: "two_seqi"
    13 
    13 
    14 "><"    ::"[o, o] => o"        (infixr 35)
    14   tens :: "[o, o] => o"        (infixr "><" 35)
    15 "-o"    ::"[o, o] => o"        (infixr 45)
    15   limp :: "[o, o] => o"        (infixr "-o" 45)
    16 "o-o"   ::"[o, o] => o"        (infixr 45)
    16   liff :: "[o, o] => o"        (infixr "o-o" 45)
    17 FShriek ::"o => o"             ("! _" [100] 1000)
    17   FShriek :: "o => o"          ("! _" [100] 1000)
    18 "&&"    ::"[o, o] => o"        (infixr 35)
    18   lconj :: "[o, o] => o"       (infixr "&&" 35)
    19 "++"    ::"[o, o] => o"        (infixr 35)
    19   ldisj :: "[o, o] => o"       (infixr "++" 35)
    20 zero    ::"o"                  ("0")
    20   zero :: "o"                  ("0")
    21 top     ::"o"                  ("1")
    21   top :: "o"                   ("1")
    22 eye     ::"o"                  ("I")
    22   eye :: "o"                   ("I")
    23 aneg    ::"o=>o"               ("~_")
    23   aneg :: "o=>o"               ("~_")
    24 
    24 
    25 
    25 
    26   (* context manipulation *)
    26   (* context manipulation *)
    27 
    27 
    28  Context      :: "two_seqi"
    28  Context      :: "two_seqi"