changeset 42814 | 5af15f1e2ef6 |
parent 41959 | b460124855b8 |
child 51309 | 473303ef6e34 |
--- a/src/Sequents/S43.thy Sun May 15 17:06:35 2011 +0200 +++ b/src/Sequents/S43.thy Sun May 15 17:45:53 2011 +0200 @@ -92,7 +92,7 @@ method_setup S43_solve = {* Scan.succeed (K (SIMPLE_METHOD (S43_Prover.solve_tac 2 ORELSE S43_Prover.solve_tac 3))) -*} "S4 solver" +*} (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)