--- 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
--- 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