# HG changeset patch
# User bulwahn
# Date 1309679965 -7200
# Node ID 9ece732627467671f8d50b14638c94319dab13c9
# Parent  5742b288bb8671f8c9f413d12843441489178c10
adding documentation of the value antiquotation to the code generation manual

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
diff -r 5742b288bb86 -r 9ece73262746 doc-src/Codegen/Thy/document/Evaluation.tex
--- 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