# HG changeset patch
# User wenzelm
# Date 967924292 -7200
# Node ID 98bb27b84363ff0faf338c314c7a0a32241080f5
# Parent  10b617bdd02883da39777d681b27c6703d4b09ca
added "slow";

diff -r 10b617bdd028 -r 98bb27b84363 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sat Sep 02 21:51:14 2000 +0200
+++ b/src/Provers/classical.ML	Sat Sep 02 21:51:32 2000 +0200
@@ -1176,6 +1176,7 @@
   ("elim", Method.thms_ctxt_args elim, "repeatedly apply elimination rules"),
   ("clarify", cla_method' clarify_tac, "repeatedly apply safe steps"),
   ("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)"),
   ("safe", cla_method safe_tac, "classical prover (apply safe rules)")];