1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Jul 20 08:16:38 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Jul 20 08:16:39 2011 +0200
     1.3 @@ -2013,6 +2013,11 @@
     1.4      \isa{{\isaliteral{22}{\isachardoublequote}}elim{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}}, and \isa{{\isaliteral{22}{\isachardoublequote}}dest{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} are passed to the appropriate proof
     1.5      methods.
     1.6  
     1.7 +  \item \hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}} attempts to prove or disprove a subgoal
     1.8 +    using a combination of provers and disprovers (\isa{{\isaliteral{22}{\isachardoublequote}}solve{\isaliteral{5F}{\isacharunderscore}}direct{\isaliteral{22}{\isachardoublequote}}},
     1.9 +    \isa{{\isaliteral{22}{\isachardoublequote}}quickcheck{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}try{\isaliteral{5F}{\isacharunderscore}}methods{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}sledgehammer{\isaliteral{22}{\isachardoublequote}}},
    1.10 +    \isa{{\isaliteral{22}{\isachardoublequote}}nitpick{\isaliteral{22}{\isachardoublequote}}}).
    1.11 +
    1.12    \item \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} attempts to prove a subgoal using external
    1.13      automatic provers (resolution provers and SMT solvers). See the Sledgehammer
    1.14      manual \cite{isabelle-sledgehammer} for details.
    1.15 @@ -2131,17 +2136,24 @@
    1.16      free variables; by default the first subgoal is tested, an other
    1.17      can be selected explicitly using an optional goal index.
    1.18      Assignments can be chosen exhausting the search space upto a given
    1.19 -    size or using a fixed number of random assignments in the search space.
    1.20 +    size, or using a fixed number of random assignments in the search space,
    1.21 +    or exploring the search space symbolically using narrowing.
    1.22      By default, quickcheck uses exhaustive testing.
    1.23      A number of configuration options are supported for
    1.24      \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}, notably:
    1.25  
    1.26      \begin{description}
    1.27  
    1.28 -    \item[\isa{tester}] specifies how to explore the search space
    1.29 -      (e.g. exhaustive or random).
    1.30 +    \item[\isa{tester}] specifies which testing approach to apply.
    1.31 +      There are three testers, \isa{exhaustive},
    1.32 +      \isa{random}, and \isa{narrowing}.
    1.33        An unknown configuration option is treated as an argument to tester,
    1.34        making \isa{{\isaliteral{22}{\isachardoublequote}}tester\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}} optional.
    1.35 +      When multiple testers are given, these are applied in parallel. 
    1.36 +      If no tester is specified, quickcheck uses the testers that are
    1.37 +      set active, i.e., configurations
    1.38 +      \isa{quickcheck{\isaliteral{5F}{\isacharunderscore}}exhaustive{\isaliteral{5F}{\isacharunderscore}}active}, \isa{quickcheck{\isaliteral{5F}{\isacharunderscore}}random{\isaliteral{5F}{\isacharunderscore}}active},
    1.39 +      \isa{quickcheck{\isaliteral{5F}{\isacharunderscore}}narrowing{\isaliteral{5F}{\isacharunderscore}}active} are set to true.
    1.40      \item[\isa{size}] specifies the maximum size of the search space
    1.41      for assignment values.
    1.42