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