added clarsimp method;
authorwenzelm
Tue, 25 Jul 2000 00:13:11 +0200
changeset 9440 a72fe5eafb5e
parent 9439 a95343122ad0
child 9441 e729ea747250
added clarsimp method;
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;