# HG changeset patch
# User wenzelm
# Date 1305325936 -7200
# Node ID 02c88bdabe752c992500e6c7fc60d7aecaa36396
# Parent  f092945f0ef7a823f4e9edde57230a2282390100
method "deepen" with optional limit;

diff -r f092945f0ef7 -r 02c88bdabe75 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Fri May 13 23:59:48 2011 +0200
+++ b/src/Provers/classical.ML	Sat May 14 00:32:16 2011 +0200
@@ -942,7 +942,9 @@
   Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depth-first)" #>
   Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depth-first)" #>
   Method.setup @{binding best} (cla_method' best_tac) "classical prover (best-first)" #>
-  Method.setup @{binding deepen} (cla_method' (fn ctxt => deepen_tac ctxt 4))
+  Method.setup @{binding deepen}
+    (Scan.lift (Scan.optional Parse.nat 4) --| Method.sections cla_modifiers
+      >> (fn n => fn ctxt => SIMPLE_METHOD' (deepen_tac ctxt n)))
     "classical prover (iterative deepening)" #>
   Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac))
     "classical prover (apply safe rules)";
diff -r f092945f0ef7 -r 02c88bdabe75 src/ZF/ex/LList.thy
--- a/src/ZF/ex/LList.thy	Fri May 13 23:59:48 2011 +0200
+++ b/src/ZF/ex/LList.thy	Sat May 14 00:32:16 2011 +0200
@@ -113,8 +113,7 @@
 apply (erule llist.cases)
 apply (simp_all add: QInl_def QInr_def llist.con_defs)
 (*LCons case: I simply can't get rid of the deepen_tac*)
-apply (tactic "deepen_tac (@{context} addIs [@{thm Ord_trans}]
-  addIs [@{thm Int_lower1} RS @{thm subset_trans}]) 2 1")
+apply (deepen 2 intro: Ord_trans Int_lower1 [THEN subset_trans])
 done
 
 lemma llist_quniv: "llist(quniv(A)) \<subseteq> quniv(A)"
@@ -216,8 +215,7 @@
 apply (erule llist.cases, simp_all)
 apply (simp_all add: QInl_def QInr_def llist.con_defs)
 (*LCons case: I simply can't get rid of the deepen_tac*)
-apply (tactic "deepen_tac (@{context} addIs [@{thm Ord_trans}]
-  addIs [@{thm Int_lower1} RS @{thm subset_trans}]) 2 1")
+apply (deepen 2 intro: Ord_trans Int_lower1 [THEN subset_trans])
 done
 
 lemma flip_in_quniv: "l \<in> llist(bool) ==> flip(l) \<in> quniv(bool)"