changeset 5985 | 9481d0cfb86e |
parent 5926 | 58f9ca06b76b |
child 7132 | 5c31d06ead04 |
--- a/src/Provers/clasimp.ML Fri Nov 27 17:01:21 1998 +0100 +++ b/src/Provers/clasimp.ML Sun Nov 29 13:13:57 1998 +0100 @@ -165,7 +165,8 @@ [Method.add_methods [("clarsimp", clasimp_method' clarsimp_tac, "clarsimp"), ("auto", clasimp_method auto_tac, "auto"), - ("force", clasimp_method' force_tac, "force")]]; + ("force", clasimp_method' force_tac, "force"), + ("brute_force", clasimp_method (ALLGOALS o force_tac), "force all goals")]]; end;