changeset 42814 | 5af15f1e2ef6 |
parent 39159 | 0dec18004e75 |
child 51309 | 473303ef6e34 |
--- a/src/Sequents/S4.thy Sun May 15 17:06:35 2011 +0200 +++ b/src/Sequents/S4.thy Sun May 15 17:45:53 2011 +0200 @@ -43,8 +43,7 @@ ) *} -method_setup S4_solve = - {* Scan.succeed (K (SIMPLE_METHOD (S4_Prover.solve_tac 2))) *} "S4 solver" +method_setup S4_solve = {* Scan.succeed (K (SIMPLE_METHOD (S4_Prover.solve_tac 2))) *} (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)