# HG changeset patch
# User wenzelm
# Date 1307651125 -7200
# Node ID dca2c7c598f0d70347b1050a42ab20dfbacdaad1
# Parent  01f051619eee20b752f7b2ee46ea85c0c3441810
document depth arguments of method "auto";

diff -r 01f051619eee -r dca2c7c598f0 doc-src/IsarRef/Thy/Generic.thy
--- a/doc-src/IsarRef/Thy/Generic.thy	Thu Jun 09 22:13:21 2011 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy	Thu Jun 09 22:25:25 2011 +0200
@@ -961,7 +961,11 @@
   ones it cannot prove.  Occasionally, attempting to prove the hard
   ones may take a long time.
 
-  %FIXME auto nat arguments
+  The optional depth arguments in @{text "(auto m n)"} refer to its
+  builtin classical reasoning procedures: @{text m} (default 4) is for
+  @{method blast}, which is tried first, and @{text n} (default 2) is
+  for a slower but more general alternative that also takes wrappers
+  into account.
 
   \item @{method force} is intended to prove the first subgoal
   completely, using many fancy proof tools and performing a rather
diff -r 01f051619eee -r dca2c7c598f0 doc-src/IsarRef/Thy/document/Generic.tex
--- a/doc-src/IsarRef/Thy/document/Generic.tex	Thu Jun 09 22:13:21 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex	Thu Jun 09 22:25:25 2011 +0200
@@ -1513,7 +1513,11 @@
   ones it cannot prove.  Occasionally, attempting to prove the hard
   ones may take a long time.
 
-  %FIXME auto nat arguments
+  The optional depth arguments in \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}auto\ m\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} refer to its
+  builtin classical reasoning procedures: \isa{m} (default 4) is for
+  \hyperlink{method.blast}{\mbox{\isa{blast}}}, which is tried first, and \isa{n} (default 2) is
+  for a slower but more general alternative that also takes wrappers
+  into account.
 
   \item \hyperlink{method.force}{\mbox{\isa{force}}} is intended to prove the first subgoal
   completely, using many fancy proof tools and performing a rather