Added "deepen" method.
authorberghofe
Fri Oct 28 17:59:07 2005 +0200 (2005-10-28)
changeset 180151cd8174b7df0
parent 18014 8bedb073e628
child 18016 8f3a80033ba4
Added "deepen" method.
src/Provers/classical.ML
     1.1 --- a/src/Provers/classical.ML	Fri Oct 28 17:27:49 2005 +0200
     1.2 +++ b/src/Provers/classical.ML	Fri Oct 28 17:59:07 2005 +0200
     1.3 @@ -1041,6 +1041,7 @@
     1.4    ("fast", cla_method' fast_tac, "classical prover (depth-first)"),
     1.5    ("slow", cla_method' slow_tac, "classical prover (slow depth-first)"),
     1.6    ("best", cla_method' best_tac, "classical prover (best-first)"),
     1.7 +  ("deepen", cla_method' (fn cs => deepen_tac cs 4), "classical prover (iterative deepening)"),
     1.8    ("safe", cla_method (CHANGED_PROP o safe_tac), "classical prover (apply safe rules)")];
     1.9  
    1.10