src/Doc/Codegen/Evaluation.thy
changeset 58100 f54a8a4134d3
parent 56927 4044a7d1720f
child 58305 57752a91eec4
     1.1 --- a/src/Doc/Codegen/Evaluation.thy	Sun Aug 31 09:10:40 2014 +0200
     1.2 +++ b/src/Doc/Codegen/Evaluation.thy	Sun Aug 31 09:10:41 2014 +0200
     1.3 @@ -93,6 +93,12 @@
     1.4    \noindent @{command value} tries first to evaluate using ML, falling
     1.5    back to normalization by evaluation if this fails.
     1.6  
     1.7 +  A particular technique may be specified in square brackets, e.g.
     1.8 +*}
     1.9 +
    1.10 +value %quote [nbe] "42 / (12 :: rat)"
    1.11 +
    1.12 +text {*
    1.13    To employ dynamic evaluation in the document generation, there is also
    1.14    a @{text value} antiquotation with the same evaluation techniques 
    1.15    as @{command value}.
    1.16 @@ -166,7 +172,10 @@
    1.17    \fontsize{9pt}{12pt}\selectfont
    1.18    \begin{tabular}{ll||c|c|c}
    1.19      & & @{text simp} & @{text nbe} & @{text code} \tabularnewline \hline \hline
    1.20 -    \multirow{4}{1ex}{\rotatebox{90}{dynamic}}
    1.21 +    \multirow{5}{1ex}{\rotatebox{90}{dynamic}}
    1.22 +      & interactive evaluation 
    1.23 +      & @{command value} @{text "[simp]"} & @{command value} @{text "[nbe]"} & @{command value} @{text "[code]"}
    1.24 +      \tabularnewline
    1.25      & plain evaluation & & & \ttsize@{ML "Code_Evaluation.dynamic_value"} \tabularnewline \cline{2-5}
    1.26      & evaluation method & @{method code_simp} & @{method normalization} & @{method eval} \tabularnewline
    1.27      & property conversion & & & \ttsize@{ML "Code_Runtime.dynamic_holds_conv"} \tabularnewline \cline{2-5}