Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed 'clarify': CHANGED;
authorwenzelm
Wed, 11 Oct 2000 00:03:22 +0200
changeset 10185 c452fea3ce74
parent 10184 4a7a1091cf65
child 10186 499637e8f2c6
fixed 'clarify': CHANGED;
src/Provers/classical.ML file | annotate | diff | comparison | revisions 
--- a/src/Provers/classical.ML	Tue Oct 10 23:44:44 2000 +0200
+++ b/src/Provers/classical.ML	Wed Oct 11 00:03:22 2000 +0200
@@ -1174,7 +1174,7 @@
   ("contradiction", Method.no_args contradiction, "proof by contradiction"),
   ("intro", Method.thms_ctxt_args intro, "repeatedly apply introduction rules"),
   ("elim", Method.thms_ctxt_args elim, "repeatedly apply elimination rules"),
-  ("clarify", cla_method' clarify_tac, "repeatedly apply safe steps"),
+  ("clarify", cla_method' (CHANGED oo clarify_tac), "repeatedly apply safe steps"),
   ("fast", cla_method' fast_tac, "classical prover (depth-first)"),
   ("slow", cla_method' slow_tac, "classical prover (slow depth-first)"),
   ("best", cla_method' best_tac, "classical prover (best-first)"),
isabelle