src/Doc/Codegen/Evaluation.thy
changeset 56927 4044a7d1720f
parent 55418 9f25e0cca254
child 58100 f54a8a4134d3
     1.1 --- a/src/Doc/Codegen/Evaluation.thy	Fri May 09 08:13:36 2014 +0200
     1.2 +++ b/src/Doc/Codegen/Evaluation.thy	Fri May 09 08:13:37 2014 +0200
     1.3 @@ -90,18 +90,12 @@
     1.4  value %quote "42 / (12 :: rat)"
     1.5  
     1.6  text {*
     1.7 -  \noindent By default @{command value} tries all available evaluation
     1.8 -  techniques and prints the result of the first succeeding one.  A particular
     1.9 -  technique may be specified in square brackets, e.g.
    1.10 -*}
    1.11 +  \noindent @{command value} tries first to evaluate using ML, falling
    1.12 +  back to normalization by evaluation if this fails.
    1.13  
    1.14 -value %quote [nbe] "42 / (12 :: rat)"
    1.15 -
    1.16 -text {*
    1.17    To employ dynamic evaluation in the document generation, there is also
    1.18 -  a @{text value} antiquotation. By default, it also tries all available evaluation
    1.19 -  techniques and prints the result of the first succeeding one, unless a particular
    1.20 -  technique is specified in square brackets.
    1.21 +  a @{text value} antiquotation with the same evaluation techniques 
    1.22 +  as @{command value}.
    1.23  
    1.24    Static evaluation freezes the code generator configuration at a
    1.25    certain point and uses this context whenever evaluation is issued
    1.26 @@ -172,10 +166,7 @@
    1.27    \fontsize{9pt}{12pt}\selectfont
    1.28    \begin{tabular}{ll||c|c|c}
    1.29      & & @{text simp} & @{text nbe} & @{text code} \tabularnewline \hline \hline
    1.30 -    \multirow{5}{1ex}{\rotatebox{90}{dynamic}}
    1.31 -      & interactive evaluation 
    1.32 -      & @{command value} @{text "[simp]"} & @{command value} @{text "[nbe]"} & @{command value} @{text "[code]"}
    1.33 -      \tabularnewline
    1.34 +    \multirow{4}{1ex}{\rotatebox{90}{dynamic}}
    1.35      & plain evaluation & & & \ttsize@{ML "Code_Evaluation.dynamic_value"} \tabularnewline \cline{2-5}
    1.36      & evaluation method & @{method code_simp} & @{method normalization} & @{method eval} \tabularnewline
    1.37      & property conversion & & & \ttsize@{ML "Code_Runtime.dynamic_holds_conv"} \tabularnewline \cline{2-5}