document depth arguments of method "auto";
authorwenzelm
Thu Jun 09 22:25:25 2011 +0200 (2011-06-09)
changeset 43332dca2c7c598f0
parent 43331 01f051619eee
child 43333 2bdec7f430d3
document depth arguments of method "auto";
doc-src/IsarRef/Thy/Generic.thy
doc-src/IsarRef/Thy/document/Generic.tex
     1.1 --- a/doc-src/IsarRef/Thy/Generic.thy	Thu Jun 09 22:13:21 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Generic.thy	Thu Jun 09 22:25:25 2011 +0200
     1.3 @@ -961,7 +961,11 @@
     1.4    ones it cannot prove.  Occasionally, attempting to prove the hard
     1.5    ones may take a long time.
     1.6  
     1.7 -  %FIXME auto nat arguments
     1.8 +  The optional depth arguments in @{text "(auto m n)"} refer to its
     1.9 +  builtin classical reasoning procedures: @{text m} (default 4) is for
    1.10 +  @{method blast}, which is tried first, and @{text n} (default 2) is
    1.11 +  for a slower but more general alternative that also takes wrappers
    1.12 +  into account.
    1.13  
    1.14    \item @{method force} is intended to prove the first subgoal
    1.15    completely, using many fancy proof tools and performing a rather
     2.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex	Thu Jun 09 22:13:21 2011 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex	Thu Jun 09 22:25:25 2011 +0200
     2.3 @@ -1513,7 +1513,11 @@
     2.4    ones it cannot prove.  Occasionally, attempting to prove the hard
     2.5    ones may take a long time.
     2.6  
     2.7 -  %FIXME auto nat arguments
     2.8 +  The optional depth arguments in \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}auto\ m\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} refer to its
     2.9 +  builtin classical reasoning procedures: \isa{m} (default 4) is for
    2.10 +  \hyperlink{method.blast}{\mbox{\isa{blast}}}, which is tried first, and \isa{n} (default 2) is
    2.11 +  for a slower but more general alternative that also takes wrappers
    2.12 +  into account.
    2.13  
    2.14    \item \hyperlink{method.force}{\mbox{\isa{force}}} is intended to prove the first subgoal
    2.15    completely, using many fancy proof tools and performing a rather