1.1 --- a/doc-src/IsarRef/Thy/Generic.thy	Sat Oct 30 15:26:40 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Generic.thy	Sat Oct 30 16:33:58 2010 +0200
     1.3 @@ -6,16 +6,15 @@
     1.4  
     1.5  section {* Configuration options *}
     1.6  
     1.7 -text {*
     1.8 -  Isabelle/Pure maintains a record of named configuration options
     1.9 -  within the theory or proof context, with values of type @{ML_type
    1.10 -  bool}, @{ML_type int}, or @{ML_type string}.  Tools may declare
    1.11 -  options in ML, and then refer to these values (relative to the
    1.12 -  context).  Thus global reference variables are easily avoided.  The
    1.13 -  user may change the value of a configuration option by means of an
    1.14 -  associated attribute of the same name.  This form of context
    1.15 -  declaration works particularly well with commands such as @{command
    1.16 -  "declare"} or @{command "using"}.
    1.17 +text {* Isabelle/Pure maintains a record of named configuration
    1.18 +  options within the theory or proof context, with values of type
    1.19 +  @{ML_type bool}, @{ML_type int}, @{ML_type real}, or @{ML_type
    1.20 +  string}.  Tools may declare options in ML, and then refer to these
    1.21 +  values (relative to the context).  Thus global reference variables
    1.22 +  are easily avoided.  The user may change the value of a
    1.23 +  configuration option by means of an associated attribute of the same
    1.24 +  name.  This form of context declaration works particularly well with
    1.25 +  commands such as @{command "declare"} or @{command "using"}.
    1.26  
    1.27    For historical reasons, some tools cannot take the full proof
    1.28    context into account and merely refer to the background theory.
    1.29 @@ -27,7 +26,7 @@
    1.30    \end{matharray}
    1.31  
    1.32    \begin{rail}
    1.33 -    name ('=' ('true' | 'false' | int | name))?
    1.34 +    name ('=' ('true' | 'false' | int | float | name))?
    1.35    \end{rail}
    1.36  
    1.37    \begin{description}