changeset 7272 | d20f51e43909 |
parent 7153 | 820c8c8573d9 |
child 7394 | 0fc6f18da7c5 |
--- a/src/Provers/clasimp.ML Wed Aug 18 20:45:52 1999 +0200 +++ b/src/Provers/clasimp.ML Wed Aug 18 20:47:31 1999 +0200 @@ -169,8 +169,8 @@ [Method.add_methods [("clarsimp", clasimp_method' clarsimp_tac, "clarsimp (improper!)"), ("auto", clasimp_method auto_tac, "auto"), - ("force", clasimp_method' force_tac, "force"), - ("brute_force", clasimp_method (ALLGOALS o force_tac), "force all goals")]]; + ("force", clasimp_method' force_tac, "force")]]; + end;