doc-src/IsarRef/Thy/document/HOL_Specific.tex

 \begin{matharray}{rcl}
     \hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isacharunderscore}format}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{attribute} \\
   \end{matharray}
 
   \begin{rail}
-    'split\_format' (((name *) + 'and') | ('(' 'complete' ')'))
+    'split\_format' ((( name * ) + 'and') | ('(' 'complete' ')'))
     ;
   \end{rail}
 
   \begin{description}
   

     'rep\_datatype' ('(' (name +) ')')? (term +)
     ;
 
     dtspec: parname? typespec infix? '=' (cons + '|')
     ;
-    cons: name (type *) mixfix?
+    cons: name ( type * ) mixfix?
   \end{rail}
 
   \begin{description}
 
   \item \hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} defines inductive datatypes in

   \end{matharray}
 
   \begin{rail}
     'relation' term
     ;
-    'lexicographic\_order' (clasimpmod *)
+    'lexicographic\_order' ( clasimpmod * )
     ;
   \end{rail}
 
   \begin{description}
 

   \begin{rail}
     'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints?
     ;
     recdeftc thmdecl? tc
     ;
-    hints: '(' 'hints' (recdefmod *) ')'
+    hints: '(' 'hints' ( recdefmod * ) ')'
     ;
     recdefmod: (('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod
     ;
     tc: nameref ('(' nat ')')?
     ;

 \begin{matharray}{rcl}
     \indexdef{HOL}{method}{iprover}\hypertarget{method.HOL.iprover}{\hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}}} & : & \isa{method} \\
   \end{matharray}
 
   \begin{rail}
-    'iprover' ('!' ?) (rulemod *)
+    'iprover' ('!' ?) ( rulemod * )
     ;
   \end{rail}
 
   The \hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}} method performs intuitionistic proof
   search, depending on specifically declared rules from the context,

   geometry.  See \hyperlink{file.~~/src/HOL/ex/Coherent.thy}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}HOL{\isacharslash}ex{\isacharslash}Coherent{\isachardot}thy}}}} for some
   examples.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isamarkupsection{Checking and refuting propositions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Identifying incorrect propositions usually involves evaluation of
+  particular assignments and systematic counter example search.  This
+  is supported by the following commands.
+
+  \begin{matharray}{rcl}
+    \indexdef{HOL}{command}{value}\hypertarget{command.HOL.value}{\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
+    \indexdef{HOL}{command}{quickcheck}\hypertarget{command.HOL.quickcheck}{\hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}{\isachardoublequote}} \\
+    \indexdef{HOL}{command}{quickcheck\_params}\hypertarget{command.HOL.quickcheck-params}{\hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isacharunderscore}params}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}}
+  \end{matharray}
+
+  \begin{rail}
+    'value' ( ( '[' name ']' ) ? ) modes? term
+    ;
+
+    'quickcheck' ( ( '[' args ']' ) ? ) nat?
+    ;
+
+    'quickcheck_params' ( ( '[' args ']' ) ? )
+    ;
+
+    modes: '(' (name + ) ')'
+    ;
+
+    args: ( name '=' value + ',' )
+    ;
+  \end{rail}
+
+  \begin{description}
+
+  \item \hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}~\isa{t} evaluates and prints a
+    term; optionally \isa{modes} can be specified, which are
+    appended to the current print mode (see also \cite{isabelle-ref}).
+    Internally, the evaluation is performed by registered evaluators,
+    which are invoked sequentially until a result is returned.
+    Alternatively a specific evaluator can be selected using square
+    brackets; available evaluators include \isa{nbe} for
+    \emph{normalization by evaluation} and \emph{code} for code
+    generation in SML.
+
+  \item \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}} tests the current goal for
+    counter examples using a series of arbitrary assignments for its
+    free variables; by default the first subgoal is tested, an other
+    can be selected explicitly using an optional goal index.
+    A number of configuration options are supported for
+    \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}, notably:
+
+    \begin{description}
+
+      \item[size] specifies the maximum size of the search space for
+        assignment values.
+
+      \item[iterations] sets how many sets of assignments are
+        generated for each particular size.
+
+    \end{description}
+
+    These option can be given within square brackets.
+
+  \item \hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isacharunderscore}params}}}} changes quickcheck
+    configuration options persitently.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isamarkupsection{Invoking automated reasoning tools -- The Sledgehammer%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%

     \indexdef{HOL}{command}{atp\_messages}\hypertarget{command.HOL.atp-messages}{\hyperlink{command.HOL.atp-messages}{\mbox{\isa{\isacommand{atp{\isacharunderscore}messages}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
     \indexdef{HOL}{method}{metis}\hypertarget{method.HOL.metis}{\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}} & : & \isa{method} \\
   \end{matharray}
 
   \begin{rail}
-  'sledgehammer' (nameref *)
+  'sledgehammer' ( nameref * )
   ;
   'atp\_messages' ('(' nat ')')?
   ;
 
   'metis' thmrefs

   One framework generates code from both functional and relational
   programs to SML.  See \cite{isabelle-HOL} for further information
   (this actually covers the new-style theory format as well).
 
   \begin{matharray}{rcl}
-    \indexdef{HOL}{command}{value}\hypertarget{command.HOL.value}{\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
     \indexdef{HOL}{command}{code\_module}\hypertarget{command.HOL.code-module}{\hyperlink{command.HOL.code-module}{\mbox{\isa{\isacommand{code{\isacharunderscore}module}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     \indexdef{HOL}{command}{code\_library}\hypertarget{command.HOL.code-library}{\hyperlink{command.HOL.code-library}{\mbox{\isa{\isacommand{code{\isacharunderscore}library}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     \indexdef{HOL}{command}{consts\_code}\hypertarget{command.HOL.consts-code}{\hyperlink{command.HOL.consts-code}{\mbox{\isa{\isacommand{consts{\isacharunderscore}code}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     \indexdef{HOL}{command}{types\_code}\hypertarget{command.HOL.types-code}{\hyperlink{command.HOL.types-code}{\mbox{\isa{\isacommand{types{\isacharunderscore}code}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\  
     \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\
   \end{matharray}
 
   \begin{rail}
-  'value' term
-  ;
-
   ( 'code\_module' | 'code\_library' ) modespec ? name ? \\
     ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\
     'contains' ( ( name '=' term ) + | term + )
   ;
 

   ;
 
   'code' (name)?
   ;
   \end{rail}
-
-  \begin{description}
-
-  \item \hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}~\isa{t} evaluates and prints a term
-  using the code generator.
-
-  \end{description}
 
   \medskip The other framework generates code from functional programs
   (including overloading using type classes) to SML \cite{SML}, OCaml
   \cite{OCaml} and Haskell \cite{haskell-revised-report}.
   Conceptually, code generation is split up in three steps: