equal
deleted
inserted
replaced
88 ) |
88 ) |
89 *} |
89 *} |
90 |
90 |
91 |
91 |
92 method_setup S43_solve = {* |
92 method_setup S43_solve = {* |
93 Scan.succeed (K (SIMPLE_METHOD |
93 Scan.succeed (fn ctxt => SIMPLE_METHOD |
94 (S43_Prover.solve_tac 2 ORELSE S43_Prover.solve_tac 3))) |
94 (S43_Prover.solve_tac ctxt 2 ORELSE S43_Prover.solve_tac ctxt 3)) |
95 *} |
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 |