1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Oct 29 11:07:21 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Oct 29 11:35:47 2010 +0200
     1.3 @@ -941,28 +941,29 @@
     1.4  
     1.5      \begin{description}
     1.6  
     1.7 -      \item[size] specifies the maximum size of the search space for
     1.8 -        assignment values.
     1.9 +    \item[@{text size}] specifies the maximum size of the search space
    1.10 +    for assignment values.
    1.11  
    1.12 -      \item[iterations] sets how many sets of assignments are
    1.13 -        generated for each particular size.
    1.14 +    \item[@{text iterations}] sets how many sets of assignments are
    1.15 +    generated for each particular size.
    1.16  
    1.17 -      \item[no\_assms] specifies whether assumptions in
    1.18 -        structured proofs should be ignored.
    1.19 +    \item[@{text no_assms}] specifies whether assumptions in
    1.20 +    structured proofs should be ignored.
    1.21  
    1.22 -      \item[timeout] sets the time limit in seconds.
    1.23 +    \item[@{text timeout}] sets the time limit in seconds.
    1.24  
    1.25 -      \item[default\_type] sets the type(s) generally used to instantiate
    1.26 -        type variables.
    1.27 +    \item[@{text default_type}] sets the type(s) generally used to
    1.28 +    instantiate type variables.
    1.29  
    1.30 -      \item[report] if set quickcheck reports how many tests fulfilled
    1.31 -        the preconditions.
    1.32 +    \item[@{text report}] if set quickcheck reports how many tests
    1.33 +    fulfilled the preconditions.
    1.34  
    1.35 -      \item[quiet] if not set quickcheck informs about the current size
    1.36 -        for assignment values.
    1.37 +    \item[@{text quiet}] if not set quickcheck informs about the
    1.38 +    current size for assignment values.
    1.39  
    1.40 -      \item[expect] can be used to check if the user's expectation was met
    1.41 -        (no\_expectation, no\_counterexample, or counterexample)
    1.42 +    \item[@{text expect}] can be used to check if the user's
    1.43 +    expectation was met (@{text no_expectation}, @{text
    1.44 +    no_counterexample}, or @{text counterexample}).
    1.45  
    1.46      \end{description}
    1.47  

     2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Oct 29 11:07:21 2010 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Oct 29 11:35:47 2010 +0200
     2.3 @@ -959,14 +959,28 @@
     2.4  
     2.5      \begin{description}
     2.6  
     2.7 -      \item[size] specifies the maximum size of the search space for
     2.8 -        assignment values.
     2.9 +    \item[\isa{size}] specifies the maximum size of the search space
    2.10 +    for assignment values.
    2.11  
    2.12 -      \item[iterations] sets how many sets of assignments are
    2.13 -        generated for each particular size.
    2.14 +    \item[\isa{iterations}] sets how many sets of assignments are
    2.15 +    generated for each particular size.
    2.16  
    2.17 -      \item[no\_assms] specifies whether assumptions in
    2.18 -        structured proofs should be ignored.
    2.19 +    \item[\isa{no{\isacharunderscore}assms}] specifies whether assumptions in
    2.20 +    structured proofs should be ignored.
    2.21 +
    2.22 +    \item[\isa{timeout}] sets the time limit in seconds.
    2.23 +
    2.24 +    \item[\isa{default{\isacharunderscore}type}] sets the type(s) generally used to
    2.25 +    instantiate type variables.
    2.26 +
    2.27 +    \item[\isa{report}] if set quickcheck reports how many tests
    2.28 +    fulfilled the preconditions.
    2.29 +
    2.30 +    \item[\isa{quiet}] if not set quickcheck informs about the
    2.31 +    current size for assignment values.
    2.32 +
    2.33 +    \item[\isa{expect}] can be used to check if the user's
    2.34 +    expectation was met (\isa{no{\isacharunderscore}expectation}, \isa{no{\isacharunderscore}counterexample}, or \isa{counterexample}).
    2.35  
    2.36      \end{description}
    2.37