# HG changeset patch
# User berghofe
# Date 1130515147 -7200
# Node ID 1cd8174b7df09a675abd81eee43cb1227f98c3c1
# Parent  8bedb073e628ff32a2909c96467b3ecd58b68cc7
Added "deepen" method.

diff -r 8bedb073e628 -r 1cd8174b7df0 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Fri Oct 28 17:27:49 2005 +0200
+++ b/src/Provers/classical.ML	Fri Oct 28 17:59:07 2005 +0200
@@ -1041,6 +1041,7 @@
   ("fast", cla_method' fast_tac, "classical prover (depth-first)"),
   ("slow", cla_method' slow_tac, "classical prover (slow depth-first)"),
   ("best", cla_method' best_tac, "classical prover (best-first)"),
+  ("deepen", cla_method' (fn cs => deepen_tac cs 4), "classical prover (iterative deepening)"),
   ("safe", cla_method (CHANGED_PROP o safe_tac), "classical prover (apply safe rules)")];