# HG changeset patch
# User wenzelm
# Date 933105600 -7200
# Node ID c47d94f61ced82da8cbaa2500840cf8fdc0b7295
# Parent  dcd7ac72f1e7dda7ee253caaf4ef40d79bdb6cf2
safe_step_tac / step_tac;

diff -r dcd7ac72f1e7 -r c47d94f61ced src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue Jul 27 21:59:23 1999 +0200
+++ b/src/Provers/classical.ML	Tue Jul 27 22:00:00 1999 +0200
@@ -1183,7 +1183,8 @@
   ("default", Method.no_args single, "apply standard rule (single step)"),
   ("contradiction", Method.no_args contradiction, "proof by contradiction"),
   ("safe_tac", cla_method safe_tac, "safe_tac"),
-  ("safe_step", cla_method' safe_step_tac, "step_tac"),
+  ("safe_step_tac", cla_method' safe_step_tac, "safe_step_tac"),
+  ("step_tac", cla_method' step_tac, "step_tac"),
   ("fast", cla_method' fast_tac, "classical prover (depth-first)"),
   ("best", cla_method' best_tac, "classical prover (best-first)"),
   ("slow", cla_method' slow_tac, "classical prover (depth-first, more backtracking)"),