equal
deleted
inserted
replaced
43 thm "rstar1", thm "rstar2"] |
43 thm "rstar1", thm "rstar2"] |
44 ) |
44 ) |
45 *} |
45 *} |
46 |
46 |
47 method_setup S4_solve = |
47 method_setup S4_solve = |
48 {* Method.no_args (Method.SIMPLE_METHOD (S4_Prover.solve_tac 2)) *} "S4 solver" |
48 {* Method.no_args (SIMPLE_METHOD (S4_Prover.solve_tac 2)) *} "S4 solver" |
49 |
49 |
50 |
50 |
51 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *) |
51 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *) |
52 |
52 |
53 lemma "|- []P --> P" by S4_solve |
53 lemma "|- []P --> P" by S4_solve |