--- 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
--- a/doc-src/Codegen/Thy/document/Evaluation.tex Sun Jul 03 08:15:14 2011 +0200
+++ b/doc-src/Codegen/Thy/document/Evaluation.tex Sun Jul 03 09:59:25 2011 +0200
@@ -152,7 +152,12 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-Static evaluation freezes the code generator configuration at a
+To employ dynamic evaluation in the document generation, there is also
+ a \isa{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
which use evaluation, since then the behaviour of evaluation is not