src/Sequents/T.ML
changeset 2073 fb0655539d05
child 17481 75166ebb619b
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Sequents/T.ML	Wed Oct 09 13:32:33 1996 +0200
     1.3 @@ -0,0 +1,17 @@
     1.4 +(*  Title:      Modal/T
     1.5 +    ID:         $Id$
     1.6 +    Author:     Martin Coen
     1.7 +    Copyright   1991  University of Cambridge
     1.8 +*)
     1.9 +
    1.10 +local open Modal0_rls T
    1.11 +in structure MP_Rule : MODAL_PROVER_RULE =
    1.12 +   struct
    1.13 +    val rewrite_rls = rewrite_rls
    1.14 +    val safe_rls    = safe_rls
    1.15 +    val unsafe_rls  = unsafe_rls @ [boxR,diaL]
    1.16 +    val bound_rls   = bound_rls @ [boxL,diaR]
    1.17 +    val aside_rls   = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2]
    1.18 +   end
    1.19 +end;
    1.20 +structure T_Prover = Modal_ProverFun(MP_Rule);