# HG changeset patch
# User paulson
# Date 844762698 -7200
# Node ID b9063086ef56e114d07aa15dda813c8883d8ac82
# Parent  b696f087f0520b697d89ad15aea81e735ea7e2bd
Introduction of Slow_tac and Slow_best_tac

diff -r b696f087f052 -r b9063086ef56 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue Oct 08 10:17:50 1996 +0200
+++ b/src/Provers/classical.ML	Tue Oct 08 10:18:18 1996 +0200
@@ -99,6 +99,8 @@
   val Step_tac 		: int -> tactic
   val Fast_tac 		: int -> tactic
   val Best_tac 		: int -> tactic
+  val Slow_tac 		: int -> tactic
+  val Slow_best_tac     : int -> tactic
   val Deepen_tac	: int -> int -> tactic
 
   end;
@@ -606,6 +608,10 @@
 
 fun Best_tac i = best_tac (!claset) i; 
 
+fun Slow_tac i = slow_tac (!claset) i; 
+
+fun Slow_best_tac i = slow_best_tac (!claset) i; 
+
 fun Deepen_tac m = deepen_tac (!claset) m; 
 
 end;