--- a/src/Provers/classical.ML Wed Jul 14 13:05:46 1999 +0200
+++ b/src/Provers/classical.ML Wed Jul 14 13:06:08 1999 +0200
@@ -1148,12 +1148,8 @@
(* contradiction *)
-(* FIXME
-val contradiction = Method.METHOD (fn facts =>
- Method.FINISHED (ALLGOALS (Method.same_tac facts THEN' (contr_tac ORELSE' assume_tac))));
-*)
-
-val contradiction = Method.METHOD (fn facts => FIRSTGOAL (Method.same_tac facts THEN' contr_tac));
+val contradiction =
+ Method.METHOD (fn facts => FIRSTGOAL (Method.same_tac facts THEN' contr_tac));
(* automatic methods *)
@@ -1188,10 +1184,10 @@
("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"),
- ("fast", cla_method' fast_tac, "fast_tac"),
- ("best", cla_method' best_tac, "best_tac"),
- ("slow", cla_method' slow_tac, "slow_tac"),
- ("slow_best", cla_method' slow_best_tac, "slow_best_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)"),
+ ("slow_best", cla_method' slow_best_tac, "classical prover (best-first, more backtracking)")];