src/Provers/classical.ML
changeset 18015 1cd8174b7df0
parent 17880 4494c023bf2a
child 18223 20830cb4428c
     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