# HG changeset patch
# User wenzelm
# Date 1307801117 -7200
# Node ID 3f1469de9e47fad635bbae91255e85885153649f
# Parent  9cbcab5c780a02760228e0267a9b55cf01fc076c
cover method "deepen" concisely;

diff -r 9cbcab5c780a -r 3f1469de9e47 doc-src/IsarRef/Thy/Generic.thy
--- a/doc-src/IsarRef/Thy/Generic.thy	Sat Jun 11 15:36:46 2011 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy	Sat Jun 11 16:05:17 2011 +0200
@@ -935,6 +935,7 @@
     @{method_def fastsimp} & : & @{text method} \\
     @{method_def slowsimp} & : & @{text method} \\
     @{method_def bestsimp} & : & @{text method} \\
+    @{method_def deepen} & : & @{text method} \\
   \end{matharray}
 
   @{rail "
@@ -949,6 +950,8 @@
     (@@{method fastsimp} | @@{method slowsimp} | @@{method bestsimp})
       (@{syntax clasimpmod} * )
     ;
+    @@{method deepen} (@{syntax nat} ?) (@{syntax clamod} * )
+    ;
     @{syntax_def clamod}:
       (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' @{syntax thmrefs}
     ;
@@ -1033,6 +1036,14 @@
   like @{method fast}, @{method slow}, @{method best}, respectively,
   but use the Simplifier as additional wrapper.
 
+  \item @{method deepen} works by exhaustive search up to a certain
+  depth.  The start depth is 4 (unless specified explicitly), and the
+  depth is increased iteratively up to 10.  Unsafe rules are modified
+  to preserve the formula they act on, so that it be used repeatedly.
+  This method can prove more goals than @{method fast}, but is much
+  slower, for example if the assumptions have many universal
+  quantifiers.
+
   \end{description}
 
   Any of the above methods support additional modifiers of the context
diff -r 9cbcab5c780a -r 3f1469de9e47 doc-src/IsarRef/Thy/document/Generic.tex
--- a/doc-src/IsarRef/Thy/document/Generic.tex	Sat Jun 11 15:36:46 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex	Sat Jun 11 16:05:17 2011 +0200
@@ -1387,6 +1387,7 @@
     \indexdef{}{method}{fastsimp}\hypertarget{method.fastsimp}{\hyperlink{method.fastsimp}{\mbox{\isa{fastsimp}}}} & : & \isa{method} \\
     \indexdef{}{method}{slowsimp}\hypertarget{method.slowsimp}{\hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}} & : & \isa{method} \\
     \indexdef{}{method}{bestsimp}\hypertarget{method.bestsimp}{\hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}}} & : & \isa{method} \\
+    \indexdef{}{method}{deepen}\hypertarget{method.deepen}{\hyperlink{method.deepen}{\mbox{\isa{deepen}}}} & : & \isa{method} \\
   \end{matharray}
 
   \begin{railoutput}
@@ -1446,6 +1447,17 @@
 \rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
 \rail@endplus
 \rail@end
+\rail@begin{2}{}
+\rail@term{\hyperlink{method.deepen}{\mbox{\isa{deepen}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
+\rail@endbar
+\rail@plus
+\rail@nextplus{1}
+\rail@cnont{\hyperlink{syntax.clamod}{\mbox{\isa{clamod}}}}[]
+\rail@endplus
+\rail@end
 \rail@begin{4}{\indexdef{}{syntax}{clamod}\hypertarget{syntax.clamod}{\hyperlink{syntax.clamod}{\mbox{\isa{clamod}}}}}
 \rail@bar
 \rail@bar
@@ -1602,6 +1614,14 @@
   like \hyperlink{method.fast}{\mbox{\isa{fast}}}, \hyperlink{method.slow}{\mbox{\isa{slow}}}, \hyperlink{method.best}{\mbox{\isa{best}}}, respectively,
   but use the Simplifier as additional wrapper.
 
+  \item \hyperlink{method.deepen}{\mbox{\isa{deepen}}} works by exhaustive search up to a certain
+  depth.  The start depth is 4 (unless specified explicitly), and the
+  depth is increased iteratively up to 10.  Unsafe rules are modified
+  to preserve the formula they act on, so that it be used repeatedly.
+  This method can prove more goals than \hyperlink{method.fast}{\mbox{\isa{fast}}}, but is much
+  slower, for example if the assumptions have many universal
+  quantifiers.
+
   \end{description}
 
   Any of the above methods support additional modifiers of the context
diff -r 9cbcab5c780a -r 3f1469de9e47 doc-src/Ref/classical.tex
--- a/doc-src/Ref/classical.tex	Sat Jun 11 15:36:46 2011 +0200
+++ b/doc-src/Ref/classical.tex	Sat Jun 11 16:05:17 2011 +0200
@@ -136,28 +136,6 @@
 \end{ttdescription}
 
 
-\subsection{Depth-limited automatic tactics}
-\begin{ttbox} 
-depth_tac  : claset -> int -> int -> tactic
-deepen_tac : claset -> int -> int -> tactic
-\end{ttbox}
-These work by exhaustive search up to a specified depth.  Unsafe rules are
-modified to preserve the formula they act on, so that it be used repeatedly.
-They can prove more goals than \texttt{fast_tac} can but are much
-slower, for example if the assumptions have many universal quantifiers.
-
-The depth limits the number of unsafe steps.  If you can estimate the minimum
-number of unsafe steps needed, supply this value as~$m$ to save time.
-\begin{ttdescription}
-\item[\ttindexbold{depth_tac} $cs$ $m$ $i$] 
-tries to prove subgoal~$i$ by exhaustive search up to depth~$m$.
-
-\item[\ttindexbold{deepen_tac} $cs$ $m$ $i$] 
-tries to prove subgoal~$i$ by iterative deepening.  It calls \texttt{depth_tac}
-repeatedly with increasing depths, starting with~$m$.
-\end{ttdescription}
-
-
 \subsection{Other useful tactics}
 \index{tactics!for contradiction}
 \index{tactics!for Modus Ponens}