Introduction of Slow_tac and Slow_best_tac
authorpaulson
Tue, 08 Oct 1996 10:18:18 +0200
changeset 2066 b9063086ef56
parent 2065 b696f087f052
child 2067 884c2eb74eb0
Introduction of Slow_tac and Slow_best_tac
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;