31 $E', P, $F'|- $G'|] ==> $E, <>P, $F |- $G" |
31 $E', P, $F'|- $G'|] ==> $E, <>P, $F |- $G" |
32 |
32 |
33 ML {* |
33 ML {* |
34 structure T_Prover = Modal_ProverFun |
34 structure T_Prover = Modal_ProverFun |
35 ( |
35 ( |
36 val rewrite_rls = thms "rewrite_rls" |
36 val rewrite_rls = @{thms rewrite_rls} |
37 val safe_rls = thms "safe_rls" |
37 val safe_rls = @{thms safe_rls} |
38 val unsafe_rls = thms "unsafe_rls" @ [thm "boxR", thm "diaL"] |
38 val unsafe_rls = @{thms unsafe_rls} @ [@{thm boxR}, @{thm diaL}] |
39 val bound_rls = thms "bound_rls" @ [thm "boxL", thm "diaR"] |
39 val bound_rls = @{thms bound_rls} @ [@{thm boxL}, @{thm diaR}] |
40 val aside_rls = [thm "lstar0", thm "lstar1", thm "lstar2", thm "rstar0", |
40 val aside_rls = [@{thm lstar0}, @{thm lstar1}, @{thm lstar2}, @{thm rstar0}, |
41 thm "rstar1", thm "rstar2"] |
41 @{thm rstar1}, @{thm rstar2}] |
42 ) |
42 ) |
43 *} |
43 *} |
44 |
44 |
45 method_setup T_solve = |
45 method_setup T_solve = |
46 {* Scan.succeed (K (SIMPLE_METHOD (T_Prover.solve_tac 2))) *} "T solver" |
46 {* Scan.succeed (K (SIMPLE_METHOD (T_Prover.solve_tac 2))) *} "T solver" |