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