src/Provers/clasimp.ML
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;