src/Sequents/S43.thy
changeset 39159 0dec18004e75
parent 35113 1a0c129bb2e0
child 41959 b460124855b8
equal deleted inserted replaced
39158:e6b96b4cde7e 39159:0dec18004e75
    77 
    77 
    78 
    78 
    79 ML {*
    79 ML {*
    80 structure S43_Prover = Modal_ProverFun
    80 structure S43_Prover = Modal_ProverFun
    81 (
    81 (
    82   val rewrite_rls = thms "rewrite_rls"
    82   val rewrite_rls = @{thms rewrite_rls}
    83   val safe_rls = thms "safe_rls"
    83   val safe_rls = @{thms safe_rls}
    84   val unsafe_rls = thms "unsafe_rls" @ [thm "pi1", thm "pi2"]
    84   val unsafe_rls = @{thms unsafe_rls} @ [@{thm pi1}, @{thm pi2}]
    85   val bound_rls = thms "bound_rls" @ [thm "boxL", thm "diaR"]
    85   val bound_rls = @{thms bound_rls} @ [@{thm boxL}, @{thm diaR}]
    86   val aside_rls = [thm "lstar0", thm "lstar1", thm "lstar2", thm "rstar0",
    86   val aside_rls = [@{thm lstar0}, @{thm lstar1}, @{thm lstar2}, @{thm rstar0},
    87     thm "rstar1", thm "rstar2", thm "S43pi0", thm "S43pi1", thm "S43pi2"]
    87     @{thm rstar1}, @{thm rstar2}, @{thm S43pi0}, @{thm S43pi1}, @{thm S43pi2}]
    88 )
    88 )
    89 *}
    89 *}
    90 
    90 
    91 
    91 
    92 method_setup S43_solve = {*
    92 method_setup S43_solve = {*