# HG changeset patch
# User paulson
# Date 859987413 -7200
# Node ID 17a23a62f82ab53314541beaf94cfdbf9f949e67
# Parent  0aa5a3cd45507526f098af8ee7b854478a972a64
New DEEPEN allows giving an upper bound for deepen_tac

diff -r 0aa5a3cd4550 -r 17a23a62f82a src/Provers/classical.ML
--- a/src/Provers/classical.ML	Wed Apr 02 15:19:40 1997 +0200
+++ b/src/Provers/classical.ML	Wed Apr 02 15:23:33 1997 +0200
@@ -14,6 +14,9 @@
 the conclusion.
 *)
 
+(*Should be a type abbreviation in signature CLASSICAL*)
+type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net;
+
 signature CLASSICAL_DATA =
   sig
   val mp	: thm    	(* [| P-->Q;  P |] ==> Q *)
@@ -32,7 +35,6 @@
 signature CLASSICAL =
   sig
   type claset
-  type netpair
   val empty_cs		: claset
   val merge_cs		: claset * claset -> claset
   val addDs 		: claset * thm list -> claset
@@ -70,7 +72,6 @@
   val best_tac 		: claset -> int -> tactic
   val slow_best_tac 	: claset -> int -> tactic
   val depth_tac		: claset -> int -> int -> tactic
-  val DEEPEN  	        : (int -> int -> tactic) -> int -> int -> tactic
   val deepen_tac	: claset -> int -> int -> tactic
 
   val contr_tac 	: int -> tactic
@@ -155,8 +156,6 @@
 
 (**** Classical rule sets ****)
 
-type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net;
-
 datatype claset =
   CS of {safeIs		: thm list,		(*safe introduction rules*)
 	 safeEs		: thm list,		(*safe elimination rules*)
@@ -607,12 +606,6 @@
 	 THEN DEPTH_SOLVE (depth_tac cs (m-1) i)))) 1)
   i);
 
-(*Iterative deepening tactical.  Allows us to "deepen" any search tactic*)
-fun DEEPEN tacf m i = STATE(fn state => 
-   if has_fewer_prems i state then no_tac
-   else (writeln ("Depth = " ^ string_of_int m);
-	 tacf m i  ORELSE  DEEPEN tacf (m+2) i));
-
 (*Search, with depth bound m.  
   This is the "entry point", which does safe inferences first.*)
 fun safe_depth_tac cs m = 
@@ -627,7 +620,7 @@
 		       DEPTH_SOLVE (deti (depth_tac cs m 1))) i
       end);
 
-fun deepen_tac cs = DEEPEN (safe_depth_tac cs);
+fun deepen_tac cs = DEEPEN (2,10) (safe_depth_tac cs);
 
 val claset = ref empty_cs;