# HG changeset patch
# User wenzelm
# Date 912341637 -3600
# Node ID 9481d0cfb86ed2682e83e90ccc4c02257bb7129f
# Parent  4c2fc177f4d33513bef084eb51da3414e2aee142
method brute_force = ALLGOALS force_tac;

diff -r 4c2fc177f4d3 -r 9481d0cfb86e src/Provers/clasimp.ML
--- 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;