src/Sequents/S4.thy
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 *)