# HG changeset patch
# User bulwahn
# Date 1320745738 -3600
# Node ID 5abb0e738b00f48ffcfc63613e4ae1a208650d91
# Parent  7156f63ce3c29308502a60b3b42b66f9150a6169
adding some documentation about the values command to the isar reference

diff -r 7156f63ce3c2 -r 5abb0e738b00 doc-src/IsarRef/Thy/HOL_Specific.thy
--- 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
diff -r 7156f63ce3c2 -r 5abb0e738b00 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- 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