changeset 43685 | 5af15f1e2ef6 |
parent 39406 | 0dec18004e75 |
child 52446 | 473303ef6e34 |
1.1 --- a/src/Sequents/S4.thy Sun May 15 17:06:35 2011 +0200 1.2 +++ b/src/Sequents/S4.thy Sun May 15 17:45:53 2011 +0200 1.3 @@ -43,8 +43,7 @@ 1.4 ) 1.5 *} 1.6 1.7 -method_setup S4_solve = 1.8 - {* Scan.succeed (K (SIMPLE_METHOD (S4_Prover.solve_tac 2))) *} "S4 solver" 1.9 +method_setup S4_solve = {* Scan.succeed (K (SIMPLE_METHOD (S4_Prover.solve_tac 2))) *} 1.10 1.11 1.12 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)