# File S4.ML

    (*  Title:      Modal/S4.ML
        ID:         $Id: S4.ML,v 1.2 2005/09/18 13:20:09 wenzelm Exp $
        Author:     Martin Coen
        Copyright   1991  University of Cambridge
    *)

    local open Modal0_rls
    in structure MP_Rule : MODAL_PROVER_RULE =
       struct
        val rewrite_rls = rewrite_rls
        val safe_rls    = safe_rls
        val unsafe_rls  = unsafe_rls @ [boxR,diaL]
        val bound_rls   = bound_rls @ [boxL,diaR]
        val aside_rls   = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2]
       end;
    end;
    structure S4_Prover = Modal_ProverFun(MP_Rule);