# HG changeset patch
# User bulwahn
# Date 1324473869 -3600
# Node ID 8c4a5e664fbc86ddd91e3d4e6c4e76b8f4b6d865
# Parent  4dfb1f6bd99b7c6b305419898389537c73778c8d
adding documentation about the quickcheck_generator command in the IsarRef

diff -r 4dfb1f6bd99b -r 8c4a5e664fbc doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Dec 21 09:41:16 2011 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Dec 21 14:24:29 2011 +0100
@@ -1522,7 +1522,8 @@
     @{command_def (HOL) "nitpick"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
     @{command_def (HOL) "quickcheck_params"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def (HOL) "refute_params"} & : & @{text "theory \<rightarrow> theory"} \\
-    @{command_def (HOL) "nitpick_params"} & : & @{text "theory \<rightarrow> theory"}
+    @{command_def (HOL) "nitpick_params"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def (HOL) "quickcheck_generator"} & : & @{text "theory \<rightarrow> theory"}
   \end{matharray}
 
   @{rail "
@@ -1539,6 +1540,9 @@
     (@@{command (HOL) quickcheck_params} | @@{command (HOL) refute_params} |
       @@{command (HOL) nitpick_params}) ( '[' args ']' )?
     ;
+    @@{command (HOL) quickcheck_generator} typeconstructor \\
+      'operations:' ( @{syntax term} +)
+    ;
 
     modes: '(' (@{syntax name} +) ')'
     ;
@@ -1630,6 +1634,11 @@
   \item @{command (HOL) "quickcheck_params"} changes
     @{command (HOL) "quickcheck"} configuration options persistently.
 
+  \item @{command (HOL) "quickcheck_generator"} creates random and
+    exhaustive value generators for a given type and operations.
+    It generates values by using the operations as if they were
+    constructors of that type.
+
   \item @{command (HOL) "refute"} tests the current goal for
     counterexamples using a reduction to SAT. The following configuration
     options are supported:
diff -r 4dfb1f6bd99b -r 8c4a5e664fbc doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Dec 21 09:41:16 2011 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Dec 21 14:24:29 2011 +0100
@@ -2217,7 +2217,8 @@
     \indexdef{HOL}{command}{nitpick}\hypertarget{command.HOL.nitpick}{\hyperlink{command.HOL.nitpick}{\mbox{\isa{\isacommand{nitpick}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
     \indexdef{HOL}{command}{quickcheck\_params}\hypertarget{command.HOL.quickcheck-params}{\hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}params}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
     \indexdef{HOL}{command}{refute\_params}\hypertarget{command.HOL.refute-params}{\hyperlink{command.HOL.refute-params}{\mbox{\isa{\isacommand{refute{\isaliteral{5F}{\isacharunderscore}}params}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
-    \indexdef{HOL}{command}{nitpick\_params}\hypertarget{command.HOL.nitpick-params}{\hyperlink{command.HOL.nitpick-params}{\mbox{\isa{\isacommand{nitpick{\isaliteral{5F}{\isacharunderscore}}params}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}}
+    \indexdef{HOL}{command}{nitpick\_params}\hypertarget{command.HOL.nitpick-params}{\hyperlink{command.HOL.nitpick-params}{\mbox{\isa{\isacommand{nitpick{\isaliteral{5F}{\isacharunderscore}}params}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
+    \indexdef{HOL}{command}{quickcheck\_generator}\hypertarget{command.HOL.quickcheck-generator}{\hyperlink{command.HOL.quickcheck-generator}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}generator}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}}
   \end{matharray}
 
   \begin{railoutput}
@@ -2281,6 +2282,16 @@
 \rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
 \rail@endbar
 \rail@end
+\rail@begin{4}{}
+\rail@term{\hyperlink{command.HOL.quickcheck-generator}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}generator}}}}}[]
+\rail@nont{\isa{typeconstructor}}[]
+\rail@cr{2}
+\rail@term{\isa{operations{\isaliteral{3A}{\isacharcolon}}}}[]
+\rail@plus
+\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
+\rail@nextplus{3}
+\rail@endplus
+\rail@end
 \rail@begin{2}{\isa{modes}}
 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
 \rail@plus
@@ -2383,6 +2394,11 @@
   \item \hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}params}}}} changes
     \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}} configuration options persistently.
 
+  \item \hyperlink{command.HOL.quickcheck-generator}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}generator}}}} creates random and
+    exhaustive value generators for a given type and operations.
+    It generates values by using the operations as if they were
+    constructors of that type.
+
   \item \hyperlink{command.HOL.refute}{\mbox{\isa{\isacommand{refute}}}} tests the current goal for
     counterexamples using a reduction to SAT. The following configuration
     options are supported: