--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Nov 08 10:33:30 2011 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Nov 08 10:48:58 2011 +0100
@@ -1513,6 +1513,7 @@
\begin{matharray}{rcl}
@{command_def (HOL) "value"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def (HOL) "values"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def (HOL) "quickcheck"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
@{command_def (HOL) "refute"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
@{command_def (HOL) "nitpick"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
@@ -1525,6 +1526,9 @@
@@{command (HOL) value} ( '[' name ']' )? modes? @{syntax term}
;
+ @@{command (HOL) values} modes? @{syntax nat}? @{syntax term}
+ ;
+
(@@{command (HOL) quickcheck} | @@{command (HOL) refute} | @@{command (HOL) nitpick})
( '[' args ']' )? @{syntax nat}?
;
@@ -1554,6 +1558,11 @@
\emph{normalization by evaluation} and \emph{code} for code
generation in SML.
+ \item @{command (HOL) "values"}~@{text t} enumerates a set comprehension
+ by evaluation and prints its values up to the given number of solutions;
+ optionally @{text modes} can be specified, which are
+ appended to the current print mode; see \secref{sec:print-modes}.
+
\item @{command (HOL) "quickcheck"} tests the current goal for
counterexamples using a series of assignments for its
free variables; by default the first subgoal is tested, an other
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Nov 08 10:33:30 2011 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Nov 08 10:48:58 2011 +0100
@@ -2207,6 +2207,7 @@
\begin{matharray}{rcl}
\indexdef{HOL}{command}{value}\hypertarget{command.HOL.value}{\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
+ \indexdef{HOL}{command}{values}\hypertarget{command.HOL.values}{\hyperlink{command.HOL.values}{\mbox{\isa{\isacommand{values}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{HOL}{command}{quickcheck}\hypertarget{command.HOL.quickcheck}{\hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}}\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}{refute}\hypertarget{command.HOL.refute}{\hyperlink{command.HOL.refute}{\mbox{\isa{\isacommand{refute}}}}}\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}{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}}} \\
@@ -2230,6 +2231,18 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
\rail@end
+\rail@begin{2}{}
+\rail@term{\hyperlink{command.HOL.values}{\mbox{\isa{\isacommand{values}}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\isa{modes}}[]
+\rail@endbar
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
+\rail@endbar
+\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
+\rail@end
\rail@begin{3}{}
\rail@bar
\rail@term{\hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}}[]
@@ -2298,6 +2311,11 @@
\emph{normalization by evaluation} and \emph{code} for code
generation in SML.
+ \item \hyperlink{command.HOL.values}{\mbox{\isa{\isacommand{values}}}}~\isa{t} enumerates a set comprehension
+ by evaluation and prints its values up to the given number of solutions;
+ optionally \isa{modes} can be specified, which are
+ appended to the current print mode; see \secref{sec:print-modes}.
+
\item \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}} tests the current goal for
counterexamples using a series of assignments for its
free variables; by default the first subgoal is tested, an other