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