# HG changeset patch
# User wenzelm
# Date 1288344947 -7200
# Node ID 6d1ebaa7a4baaee00cfd4731138b35587111afcb
# Parent  f99ec71de82db6486451075945df4159f2003863
proper markup of formal text;

diff -r f99ec71de82d -r 6d1ebaa7a4ba doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Oct 29 11:07:21 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Oct 29 11:35:47 2010 +0200
@@ -941,28 +941,29 @@
 
     \begin{description}
 
-      \item[size] specifies the maximum size of the search space for
-        assignment values.
+    \item[@{text size}] specifies the maximum size of the search space
+    for assignment values.
 
-      \item[iterations] sets how many sets of assignments are
-        generated for each particular size.
+    \item[@{text iterations}] sets how many sets of assignments are
+    generated for each particular size.
 
-      \item[no\_assms] specifies whether assumptions in
-        structured proofs should be ignored.
+    \item[@{text no_assms}] specifies whether assumptions in
+    structured proofs should be ignored.
 
-      \item[timeout] sets the time limit in seconds.
+    \item[@{text timeout}] sets the time limit in seconds.
 
-      \item[default\_type] sets the type(s) generally used to instantiate
-        type variables.
+    \item[@{text 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[@{text 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[@{text 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)
+    \item[@{text expect}] can be used to check if the user's
+    expectation was met (@{text no_expectation}, @{text
+    no_counterexample}, or @{text counterexample}).
 
     \end{description}
 
diff -r f99ec71de82d -r 6d1ebaa7a4ba doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Oct 29 11:07:21 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Oct 29 11:35:47 2010 +0200
@@ -959,14 +959,28 @@
 
     \begin{description}
 
-      \item[size] specifies the maximum size of the search space for
-        assignment values.
+    \item[\isa{size}] specifies the maximum size of the search space
+    for assignment values.
+
+    \item[\isa{iterations}] sets how many sets of assignments are
+    generated for each particular size.
+
+    \item[\isa{no{\isacharunderscore}assms}] specifies whether assumptions in
+    structured proofs should be ignored.
+
+    \item[\isa{timeout}] sets the time limit in seconds.
 
-      \item[iterations] sets how many sets of assignments are
-        generated for each particular size.
+    \item[\isa{default{\isacharunderscore}type}] sets the type(s) generally used to
+    instantiate type variables.
+
+    \item[\isa{report}] if set quickcheck reports how many tests
+    fulfilled the preconditions.
 
-      \item[no\_assms] specifies whether assumptions in
-        structured proofs should be ignored.
+    \item[\isa{quiet}] if not set quickcheck informs about the
+    current size for assignment values.
+
+    \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}).
 
     \end{description}