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