# HG changeset patch
# User wenzelm
# Date 967761099 -7200
# Node ID c5024f705d2492983a5eac7701f151a9af771ad7
# Parent  c07777210a693f1ba7e0f4b96f62c787e544241f
added "safe" method;

diff -r c07777210a69 -r c5024f705d24 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Fri Sep 01 00:31:08 2000 +0200
+++ b/src/Provers/classical.ML	Fri Sep 01 00:31:39 2000 +0200
@@ -1176,7 +1176,8 @@
   ("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)"),
-  ("best", cla_method' best_tac, "classical prover (best-first)")];
+  ("best", cla_method' best_tac, "classical prover (best-first)"),
+  ("safe", cla_method safe_tac, "classical prover (apply safe rules)")];