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