Introduction of Slow_tac and Slow_best_tac
authorpaulson
Tue Oct 08 10:18:18 1996 +0200 (1996-10-08)
changeset 2066b9063086ef56
parent 2065 b696f087f052
child 2067 884c2eb74eb0
Introduction of Slow_tac and Slow_best_tac
src/Provers/classical.ML
     1.1 --- a/src/Provers/classical.ML	Tue Oct 08 10:17:50 1996 +0200
     1.2 +++ b/src/Provers/classical.ML	Tue Oct 08 10:18:18 1996 +0200
     1.3 @@ -99,6 +99,8 @@
     1.4    val Step_tac 		: int -> tactic
     1.5    val Fast_tac 		: int -> tactic
     1.6    val Best_tac 		: int -> tactic
     1.7 +  val Slow_tac 		: int -> tactic
     1.8 +  val Slow_best_tac     : int -> tactic
     1.9    val Deepen_tac	: int -> int -> tactic
    1.10  
    1.11    end;
    1.12 @@ -606,6 +608,10 @@
    1.13  
    1.14  fun Best_tac i = best_tac (!claset) i; 
    1.15  
    1.16 +fun Slow_tac i = slow_tac (!claset) i; 
    1.17 +
    1.18 +fun Slow_best_tac i = slow_best_tac (!claset) i; 
    1.19 +
    1.20  fun Deepen_tac m = deepen_tac (!claset) m; 
    1.21  
    1.22  end;