src/Provers/classical.ML
changeset 10185 c452fea3ce74
parent 10034 4bca6b2d2589
child 10309 a7f961fb62c6
     1.1 --- a/src/Provers/classical.ML	Tue Oct 10 23:44:44 2000 +0200
     1.2 +++ b/src/Provers/classical.ML	Wed Oct 11 00:03:22 2000 +0200
     1.3 @@ -1174,7 +1174,7 @@
     1.4    ("contradiction", Method.no_args contradiction, "proof by contradiction"),
     1.5    ("intro", Method.thms_ctxt_args intro, "repeatedly apply introduction rules"),
     1.6    ("elim", Method.thms_ctxt_args elim, "repeatedly apply elimination rules"),
     1.7 -  ("clarify", cla_method' clarify_tac, "repeatedly apply safe steps"),
     1.8 +  ("clarify", cla_method' (CHANGED oo clarify_tac), "repeatedly apply safe steps"),
     1.9    ("fast", cla_method' fast_tac, "classical prover (depth-first)"),
    1.10    ("slow", cla_method' slow_tac, "classical prover (slow depth-first)"),
    1.11    ("best", cla_method' best_tac, "classical prover (best-first)"),