1.1 --- a/doc-src/Codegen/Thy/Evaluation.thy	Sun Jul 03 08:15:14 2011 +0200
     1.2 +++ b/doc-src/Codegen/Thy/Evaluation.thy	Sun Jul 03 09:59:25 2011 +0200
     1.3 @@ -98,6 +98,11 @@
     1.4  value %quote [nbe] "42 / (12 :: rat)"
     1.5  
     1.6  text {*
     1.7 +  To employ dynamic evaluation in the document generation, there is also
     1.8 +  a @{text value} antiquotation. By default, it also tries all available evaluation
     1.9 +  techniques and prints the result of the first succeeding one, unless a particular
    1.10 +  technique is specified in square brackets.
    1.11 +
    1.12    Static evaluation freezes the code generator configuration at a
    1.13    certain point and uses this context whenever evaluation is issued
    1.14    later on.  This is particularly appropriate for proof procedures

     2.1 --- a/doc-src/Codegen/Thy/document/Evaluation.tex	Sun Jul 03 08:15:14 2011 +0200
     2.2 +++ b/doc-src/Codegen/Thy/document/Evaluation.tex	Sun Jul 03 09:59:25 2011 +0200
     2.3 @@ -152,7 +152,12 @@
     2.4  \endisadelimquote
     2.5  %
     2.6  \begin{isamarkuptext}%
     2.7 -Static evaluation freezes the code generator configuration at a
     2.8 +To employ dynamic evaluation in the document generation, there is also
     2.9 +  a \isa{value} antiquotation. By default, it also tries all available evaluation
    2.10 +  techniques and prints the result of the first succeeding one, unless a particular
    2.11 +  technique is specified in square brackets.
    2.12 +
    2.13 +  Static evaluation freezes the code generator configuration at a
    2.14    certain point and uses this context whenever evaluation is issued
    2.15    later on.  This is particularly appropriate for proof procedures
    2.16    which use evaluation, since then the behaviour of evaluation is not