# HG changeset patch
# User bulwahn
# Date 1329930521 -3600
# Node ID d5d49bd4a7b452f515a9f3acf91f0c94441db0e5
# Parent  1116909ef176775dfa20703ce53e4221f8ed8be0
adding documentation about find_unused_assms command and use_subtype option in the IsarRef

diff -r 1116909ef176 -r d5d49bd4a7b4 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Feb 22 18:08:27 2012 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Feb 22 18:08:41 2012 +0100
@@ -1643,7 +1643,8 @@
     @{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) "quickcheck_generator"} & : & @{text "theory \<rightarrow> theory"}
+    @{command_def (HOL) "quickcheck_generator"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def (HOL) "find_unused_assms"} & : & @{text "context \<rightarrow>"}
   \end{matharray}
 
   @{rail "
@@ -1660,10 +1661,14 @@
     (@@{command (HOL) quickcheck_params} | @@{command (HOL) refute_params} |
       @@{command (HOL) nitpick_params}) ( '[' args ']' )?
     ;
+
     @@{command (HOL) quickcheck_generator} typeconstructor \\
       'operations:' ( @{syntax term} +)
     ;
 
+    @@{command (HOL) find_unused_assms} theoryname?
+    ;
+
     modes: '(' (@{syntax name} +) ')'
     ;
 
@@ -1743,6 +1748,10 @@
     \item[@{text report}] if set quickcheck reports how many tests
     fulfilled the preconditions.
 
+    \item[@{text use_subtype}] if set quickcheck automatically lifts
+    conjectures to registered subtypes if possible, and tests the
+    lifted conjecture.
+
     \item[@{text quiet}] if set quickcheck does not output anything
     while testing.
     
@@ -1806,6 +1815,13 @@
   \item @{command (HOL) "nitpick_params"} changes @{command (HOL)
   "nitpick"} configuration options persistently.
 
+  \item @{command (HOL) "find_unused_assms"} finds potentially superfluous
+  assumptions in theorems using quickcheck.
+  It takes the theory name to be checked for superfluous assumptions as
+  optional argument. If not provided, it checks the current theory.
+  Options to the internal quickcheck invocations can be changed with
+  common configuration declarations.
+
   \end{description}
 *}
 
diff -r 1116909ef176 -r d5d49bd4a7b4 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Feb 22 18:08:27 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Feb 22 18:08:41 2012 +0100
@@ -2341,7 +2341,8 @@
     \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}{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}}}
+    \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}}} \\
+    \indexdef{HOL}{command}{find\_unused\_assms}\hypertarget{command.HOL.find-unused-assms}{\hyperlink{command.HOL.find-unused-assms}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}unused{\isaliteral{5F}{\isacharunderscore}}assms}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}}
   \end{matharray}
 
   \begin{railoutput}
@@ -2415,6 +2416,13 @@
 \rail@nextplus{3}
 \rail@endplus
 \rail@end
+\rail@begin{2}{}
+\rail@term{\hyperlink{command.HOL.find-unused-assms}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}unused{\isaliteral{5F}{\isacharunderscore}}assms}}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\isa{theoryname}}[]
+\rail@endbar
+\rail@end
 \rail@begin{2}{\isa{modes}}
 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
 \rail@plus
@@ -2504,6 +2512,10 @@
     \item[\isa{report}] if set quickcheck reports how many tests
     fulfilled the preconditions.
 
+    \item[\isa{use{\isaliteral{5F}{\isacharunderscore}}subtype}] if set quickcheck automatically lifts
+    conjectures to registered subtypes if possible, and tests the
+    lifted conjecture.
+
     \item[\isa{quiet}] if set quickcheck does not output anything
     while testing.
     
@@ -2562,6 +2574,13 @@
 
   \item \hyperlink{command.HOL.nitpick-params}{\mbox{\isa{\isacommand{nitpick{\isaliteral{5F}{\isacharunderscore}}params}}}} changes \hyperlink{command.HOL.nitpick}{\mbox{\isa{\isacommand{nitpick}}}} configuration options persistently.
 
+  \item \hyperlink{command.HOL.find-unused-assms}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}unused{\isaliteral{5F}{\isacharunderscore}}assms}}}} finds potentially superfluous
+  assumptions in theorems using quickcheck.
+  It takes the theory name to be checked for superfluous assumptions as
+  optional argument. If not provided, it checks the current theory.
+  Options to the internal quickcheck invocations can be changed with
+  common configuration declarations.
+
   \end{description}%
 \end{isamarkuptext}%
 \isamarkuptrue%