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