--- a/doc-src/IsarRef/Thy/Generic.thy Sat Oct 30 15:26:40 2010 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy Sat Oct 30 16:33:58 2010 +0200
@@ -6,16 +6,15 @@
section {* Configuration options *}
-text {*
- Isabelle/Pure maintains a record of named configuration options
- within the theory or proof context, with values of type @{ML_type
- bool}, @{ML_type int}, or @{ML_type string}. Tools may declare
- options in ML, and then refer to these values (relative to the
- context). Thus global reference variables are easily avoided. The
- user may change the value of a configuration option by means of an
- associated attribute of the same name. This form of context
- declaration works particularly well with commands such as @{command
- "declare"} or @{command "using"}.
+text {* Isabelle/Pure maintains a record of named configuration
+ options within the theory or proof context, with values of type
+ @{ML_type bool}, @{ML_type int}, @{ML_type real}, or @{ML_type
+ string}. Tools may declare options in ML, and then refer to these
+ values (relative to the context). Thus global reference variables
+ are easily avoided. The user may change the value of a
+ configuration option by means of an associated attribute of the same
+ name. This form of context declaration works particularly well with
+ commands such as @{command "declare"} or @{command "using"}.
For historical reasons, some tools cannot take the full proof
context into account and merely refer to the background theory.
@@ -27,7 +26,7 @@
\end{matharray}
\begin{rail}
- name ('=' ('true' | 'false' | int | name))?
+ name ('=' ('true' | 'false' | int | float | name))?
\end{rail}
\begin{description}