Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Now deepen_tac can take advantage of wrappers --
authorpaulson
Thu, 22 Aug 1996 12:27:01 +0200
changeset 1938 4e29ea45520d
parent 1937 e59ff0eb1e91
child 1939 ad5bb12605fb
Now deepen_tac can take advantage of wrappers -- including addss...
src/Provers/classical.ML file | annotate | diff | comparison | revisions 
--- a/src/Provers/classical.ML	Thu Aug 22 12:24:58 1996 +0200
+++ b/src/Provers/classical.ML	Thu Aug 22 12:27:01 1996 +0200
@@ -66,6 +66,7 @@
   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
@@ -550,12 +551,13 @@
 (*Searching to depth m.*)
 fun depth_tac cs m i = STATE(fn state => 
   SELECT_GOAL 
+   (getwrapper cs
     (REPEAT_DETERM1 (safe_step_tac cs 1) THEN_ELSE
      (DEPTH_SOLVE (depth_tac cs m 1),
       inst0_step_tac cs 1  APPEND
       COND (K(m=0)) no_tac
         ((instp_step_tac cs 1 APPEND dup_step_tac cs 1)
-	 THEN DEPTH_SOLVE (depth_tac cs (m-1) 1))))
+	 THEN DEPTH_SOLVE (depth_tac cs (m-1) 1)))))
   i);
 
 (*Iterative deepening tactical.  Allows us to "deepen" any search tactic*)
isabelle