method brute_force = ALLGOALS force_tac;

--- 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;