--- a/src/Doc/Codegen/Evaluation.thy Sun Aug 31 09:10:40 2014 +0200
+++ b/src/Doc/Codegen/Evaluation.thy Sun Aug 31 09:10:41 2014 +0200
@@ -93,6 +93,12 @@
\noindent @{command value} tries first to evaluate using ML, falling
back to normalization by evaluation if this fails.
+ A particular technique may be specified in square brackets, e.g.
+*}
+
+value %quote [nbe] "42 / (12 :: rat)"
+
+text {*
To employ dynamic evaluation in the document generation, there is also
a @{text value} antiquotation with the same evaluation techniques
as @{command value}.
@@ -166,7 +172,10 @@
\fontsize{9pt}{12pt}\selectfont
\begin{tabular}{ll||c|c|c}
& & @{text simp} & @{text nbe} & @{text code} \tabularnewline \hline \hline
- \multirow{4}{1ex}{\rotatebox{90}{dynamic}}
+ \multirow{5}{1ex}{\rotatebox{90}{dynamic}}
+ & interactive evaluation
+ & @{command value} @{text "[simp]"} & @{command value} @{text "[nbe]"} & @{command value} @{text "[code]"}
+ \tabularnewline
& plain evaluation & & & \ttsize@{ML "Code_Evaluation.dynamic_value"} \tabularnewline \cline{2-5}
& evaluation method & @{method code_simp} & @{method normalization} & @{method eval} \tabularnewline
& property conversion & & & \ttsize@{ML "Code_Runtime.dynamic_holds_conv"} \tabularnewline \cline{2-5}