src/Sequents/LK.thy
changeset 17481 75166ebb619b
parent 7117 37eccadf6b8a
child 21428 f84cf8e9cad8
equal deleted inserted replaced
17480:fd19f77dcf60 17481:75166ebb619b
     1 (*  Title:      LK/LK
     1 (*  Title:      LK/LK.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     4     Copyright   1993  University of Cambridge
     5 
     5 
     6 Axiom to express monotonicity (a variant of the deduction theorem).  Makes the
     6 Axiom to express monotonicity (a variant of the deduction theorem).  Makes the
    11 
    11 
    12 CANNOT be added to LK0.thy because modal logic is built upon it, and
    12 CANNOT be added to LK0.thy because modal logic is built upon it, and
    13 various modal rules would become inconsistent.
    13 various modal rules would become inconsistent.
    14 *)
    14 *)
    15 
    15 
    16 LK = LK0 +
    16 theory LK
       
    17 imports LK0
       
    18 uses ("simpdata.ML")
       
    19 begin
    17 
    20 
    18 rules
    21 axioms
    19 
    22 
    20   monotonic  "($H |- P ==> $H |- Q) ==> $H, P |- Q"
    23   monotonic:  "($H |- P ==> $H |- Q) ==> $H, P |- Q"
    21 
    24 
    22   left_cong  "[| P == P';  |- P' ==> ($H |- $F) == ($H' |- $F') |] 
    25   left_cong:  "[| P == P';  |- P' ==> ($H |- $F) == ($H' |- $F') |]
    23               ==> (P, $H |- $F) == (P', $H' |- $F')"
    26                ==> (P, $H |- $F) == (P', $H' |- $F')"
       
    27 
       
    28 ML {* use_legacy_bindings (the_context ()) *}
       
    29 
       
    30 use "simpdata.ML"
       
    31 
    24 end
    32 end