1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Jul 20 08:16:38 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Jul 20 08:16:39 2011 +0200
     1.3 @@ -1382,6 +1382,11 @@
     1.4      @{text "elim:"}, and @{text "dest:"} are passed to the appropriate proof
     1.5      methods.
     1.6  
     1.7 +  \item @{command (HOL) "try"} attempts to prove or disprove a subgoal
     1.8 +    using a combination of provers and disprovers (@{text "solve_direct"},
     1.9 +    @{text "quickcheck"}, @{text "try_methods"}, @{text "sledgehammer"},
    1.10 +    @{text "nitpick"}).
    1.11 +
    1.12    \item @{command (HOL) "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 @@ -1448,17 +1453,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      @{command (HOL) "quickcheck"}, notably:
    1.25  
    1.26      \begin{description}
    1.27  
    1.28 -    \item[@{text tester}] specifies how to explore the search space
    1.29 -      (e.g. exhaustive or random).
    1.30 +    \item[@{text tester}] specifies which testing approach to apply.
    1.31 +      There are three testers, @{text exhaustive},
    1.32 +      @{text random}, and @{text narrowing}.
    1.33        An unknown configuration option is treated as an argument to tester,
    1.34        making @{text "tester ="} 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 +      @{text quickcheck_exhaustive_active}, @{text quickcheck_random_active},
    1.39 +      @{text quickcheck_narrowing_active} are set to true.
    1.40      \item[@{text size}] specifies the maximum size of the search space
    1.41      for assignment values.
    1.42  

     2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Jul 20 08:16:38 2011 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Jul 20 08:16:39 2011 +0200
     2.3 @@ -2013,6 +2013,11 @@
     2.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
     2.5      methods.
     2.6  
     2.7 +  \item \hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}} attempts to prove or disprove a subgoal
     2.8 +    using a combination of provers and disprovers (\isa{{\isaliteral{22}{\isachardoublequote}}solve{\isaliteral{5F}{\isacharunderscore}}direct{\isaliteral{22}{\isachardoublequote}}},
     2.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}}},
    2.10 +    \isa{{\isaliteral{22}{\isachardoublequote}}nitpick{\isaliteral{22}{\isachardoublequote}}}).
    2.11 +
    2.12    \item \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} attempts to prove a subgoal using external
    2.13      automatic provers (resolution provers and SMT solvers). See the Sledgehammer
    2.14      manual \cite{isabelle-sledgehammer} for details.
    2.15 @@ -2131,17 +2136,24 @@
    2.16      free variables; by default the first subgoal is tested, an other
    2.17      can be selected explicitly using an optional goal index.
    2.18      Assignments can be chosen exhausting the search space upto a given
    2.19 -    size or using a fixed number of random assignments in the search space.
    2.20 +    size, or using a fixed number of random assignments in the search space,
    2.21 +    or exploring the search space symbolically using narrowing.
    2.22      By default, quickcheck uses exhaustive testing.
    2.23      A number of configuration options are supported for
    2.24      \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}, notably:
    2.25  
    2.26      \begin{description}
    2.27  
    2.28 -    \item[\isa{tester}] specifies how to explore the search space
    2.29 -      (e.g. exhaustive or random).
    2.30 +    \item[\isa{tester}] specifies which testing approach to apply.
    2.31 +      There are three testers, \isa{exhaustive},
    2.32 +      \isa{random}, and \isa{narrowing}.
    2.33        An unknown configuration option is treated as an argument to tester,
    2.34        making \isa{{\isaliteral{22}{\isachardoublequote}}tester\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}} optional.
    2.35 +      When multiple testers are given, these are applied in parallel. 
    2.36 +      If no tester is specified, quickcheck uses the testers that are
    2.37 +      set active, i.e., configurations
    2.38 +      \isa{quickcheck{\isaliteral{5F}{\isacharunderscore}}exhaustive{\isaliteral{5F}{\isacharunderscore}}active}, \isa{quickcheck{\isaliteral{5F}{\isacharunderscore}}random{\isaliteral{5F}{\isacharunderscore}}active},
    2.39 +      \isa{quickcheck{\isaliteral{5F}{\isacharunderscore}}narrowing{\isaliteral{5F}{\isacharunderscore}}active} are set to true.
    2.40      \item[\isa{size}] specifies the maximum size of the search space
    2.41      for assignment values.
    2.42