# HG changeset patch
# User wenzelm
# Date 1288982365 -3600
# Node ID ae4b67af2f37dd8f1ae4123e5fd46da3cbee2a93
# Parent  7ea01f842830f4fc85612ed03ddf46d4bf9fb495
updated generated file, overwriting 55a1693affb6 whose content appears to be in the thy source already;

diff -r 7ea01f842830 -r ae4b67af2f37 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Nov 05 19:22:04 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Nov 05 19:39:25 2010 +0100
@@ -982,20 +982,6 @@
     \item[\isa{expect}] can be used to check if the user's
     expectation was met (\isa{no{\isacharunderscore}expectation}, \isa{no{\isacharunderscore}counterexample}, or \isa{counterexample}).
 
-      \item[timeout] sets the time limit in seconds.
-
-      \item[default\_type] sets the type(s) generally used to instantiate
-        type variables.
-
-      \item[report] if set quickcheck reports how many tests fulfilled
-        the preconditions.
-
-      \item[quiet] if not set quickcheck informs about the current size
-        for assignment values.
-
-      \item[expect] can be used to check if the user's expectation was met
-        (no\_expectation, no\_counterexample, or counterexample)
-
     \end{description}
 
     These option can be given within square brackets.