added "safe" method;
authorwenzelm
Fri Sep 01 00:31:39 2000 +0200 (2000-09-01 ago)
changeset 9773c5024f705d24
parent 9772 c07777210a69
child 9774 e745a418e6a5
added "safe" method;
src/Provers/classical.ML
     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