src/Sequents/LK.thy
changeset 17481 75166ebb619b
parent 7117 37eccadf6b8a
child 21428 f84cf8e9cad8
     1.1 --- a/src/Sequents/LK.thy	Sun Sep 18 14:25:48 2005 +0200
     1.2 +++ b/src/Sequents/LK.thy	Sun Sep 18 15:20:08 2005 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      LK/LK
     1.5 +(*  Title:      LK/LK.ML
     1.6      ID:         $Id$
     1.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   1993  University of Cambridge
     1.9 @@ -13,12 +13,20 @@
    1.10  various modal rules would become inconsistent.
    1.11  *)
    1.12  
    1.13 -LK = LK0 +
    1.14 +theory LK
    1.15 +imports LK0
    1.16 +uses ("simpdata.ML")
    1.17 +begin
    1.18  
    1.19 -rules
    1.20 +axioms
    1.21 +
    1.22 +  monotonic:  "($H |- P ==> $H |- Q) ==> $H, P |- Q"
    1.23  
    1.24 -  monotonic  "($H |- P ==> $H |- Q) ==> $H, P |- Q"
    1.25 +  left_cong:  "[| P == P';  |- P' ==> ($H |- $F) == ($H' |- $F') |]
    1.26 +               ==> (P, $H |- $F) == (P', $H' |- $F')"
    1.27  
    1.28 -  left_cong  "[| P == P';  |- P' ==> ($H |- $F) == ($H' |- $F') |] 
    1.29 -              ==> (P, $H |- $F) == (P', $H' |- $F')"
    1.30 +ML {* use_legacy_bindings (the_context ()) *}
    1.31 +
    1.32 +use "simpdata.ML"
    1.33 +
    1.34  end