src/Provers/clasimp.ML

--- a/src/Provers/clasimp.ML	Tue Jul 25 00:12:50 2000 +0200
+++ b/src/Provers/clasimp.ML	Tue Jul 25 00:13:11 2000 +0200
@@ -193,10 +193,9 @@
 
 val setup =
  [Method.add_methods
-   [("clarsimp_tac", clasimp_method' clarsimp_tac, "clarsimp (improper!)"),
+   [("force", clasimp_method' force_tac, "force"),
     ("auto", clasimp_method (CHANGED o auto_tac), "auto"),
-    ("force", clasimp_method' force_tac, "force")]];
-    
+    ("clarsimp", clasimp_method' clarsimp_tac, "clarify simplified goal")]];
 
 
 end;