Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
safe_step_tac / step_tac;
authorwenzelm
Tue, 27 Jul 1999 22:00:00 +0200
changeset 7106 c47d94f61ced
parent 7105 dcd7ac72f1e7
child 7107 ce69de572bca
safe_step_tac / step_tac;
src/Provers/classical.ML file | annotate | diff | comparison | revisions 
--- 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)"),
isabelle