src/Provers/classical.ML
changeset 9773 c5024f705d24
parent 9760 72c0a12ae3bf
child 9806 98bb27b84363
     1.1 --- a/src/Provers/classical.ML	Fri Sep 01 00:31:08 2000 +0200
     1.2 +++ b/src/Provers/classical.ML	Fri Sep 01 00:31:39 2000 +0200
     1.3 @@ -1176,7 +1176,8 @@
     1.4    ("elim", Method.thms_ctxt_args elim, "repeatedly apply elimination rules"),
     1.5    ("clarify", cla_method' clarify_tac, "repeatedly apply safe steps"),
     1.6    ("fast", cla_method' fast_tac, "classical prover (depth-first)"),
     1.7 -  ("best", cla_method' best_tac, "classical prover (best-first)")];
     1.8 +  ("best", cla_method' best_tac, "classical prover (best-first)"),
     1.9 +  ("safe", cla_method safe_tac, "classical prover (apply safe rules)")];
    1.10  
    1.11  
    1.12