src/Sequents/S4.thy
changeset 30510 4120fc59dd85
parent 21590 ef7278f553eb
child 30549 d2d7874648bd
     1.1 --- a/src/Sequents/S4.thy	Fri Mar 13 19:53:09 2009 +0100
     1.2 +++ b/src/Sequents/S4.thy	Fri Mar 13 19:58:26 2009 +0100
     1.3 @@ -45,7 +45,7 @@
     1.4  *}
     1.5  
     1.6  method_setup S4_solve =
     1.7 -  {* Method.no_args (Method.SIMPLE_METHOD (S4_Prover.solve_tac 2)) *} "S4 solver"
     1.8 +  {* Method.no_args (SIMPLE_METHOD (S4_Prover.solve_tac 2)) *} "S4 solver"
     1.9  
    1.10  
    1.11  (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)