src/Sequents/Modal0.thy
changeset 14765 bafb24c150c1
parent 7098 86583034aacf
child 17481 75166ebb619b
equal deleted inserted replaced
14764:5d8a9900cabc 14765:bafb24c150c1
     8 
     8 
     9 consts
     9 consts
    10   box           :: "o=>o"       ("[]_" [50] 50)
    10   box           :: "o=>o"       ("[]_" [50] 50)
    11   dia           :: "o=>o"       ("<>_" [50] 50)
    11   dia           :: "o=>o"       ("<>_" [50] 50)
    12   "--<",">-<"   :: "[o,o]=>o"   (infixr 25)
    12   "--<",">-<"   :: "[o,o]=>o"   (infixr 25)
       
    13   Lstar,Rstar   :: "two_seqi"
       
    14 
       
    15 syntax
    13   "@Lstar"      :: "two_seqe"   ("(_)|L>(_)" [6,6] 5)
    16   "@Lstar"      :: "two_seqe"   ("(_)|L>(_)" [6,6] 5)
    14   "@Rstar"      :: "two_seqe"   ("(_)|R>(_)" [6,6] 5)
    17   "@Rstar"      :: "two_seqe"   ("(_)|R>(_)" [6,6] 5)
    15   Lstar,Rstar   :: "two_seqi"
       
    16 
    18 
    17 rules
    19 rules
    18   (* Definitions *)
    20   (* Definitions *)
    19 
    21 
    20   strimp_def    "P --< Q == [](P --> Q)"
    22   strimp_def    "P --< Q == [](P --> Q)"