equal
deleted
inserted
replaced
90 |
90 |
91 |
91 |
92 method_setup S43_solve = {* |
92 method_setup S43_solve = {* |
93 Scan.succeed (K (SIMPLE_METHOD |
93 Scan.succeed (K (SIMPLE_METHOD |
94 (S43_Prover.solve_tac 2 ORELSE S43_Prover.solve_tac 3))) |
94 (S43_Prover.solve_tac 2 ORELSE S43_Prover.solve_tac 3))) |
95 *} "S4 solver" |
95 *} |
96 |
96 |
97 |
97 |
98 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *) |
98 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *) |
99 |
99 |
100 lemma "|- []P --> P" by S43_solve |
100 lemma "|- []P --> P" by S43_solve |