adding documentation of the value antiquotation to the code generation manual
authorbulwahn
Sun Jul 03 09:59:25 2011 +0200 (2011-07-03)
changeset 436569ece73262746
parent 43655 5742b288bb86
child 43657 537ea3846f64
child 43686 bc7d63c7fd6f
adding documentation of the value antiquotation to the code generation manual
doc-src/Codegen/Thy/Evaluation.thy
doc-src/Codegen/Thy/document/Evaluation.tex
     1.1 --- a/doc-src/Codegen/Thy/Evaluation.thy	Sun Jul 03 08:15:14 2011 +0200
     1.2 +++ b/doc-src/Codegen/Thy/Evaluation.thy	Sun Jul 03 09:59:25 2011 +0200
     1.3 @@ -98,6 +98,11 @@
     1.4  value %quote [nbe] "42 / (12 :: rat)"
     1.5  
     1.6  text {*
     1.7 +  To employ dynamic evaluation in the document generation, there is also
     1.8 +  a @{text value} antiquotation. By default, it also tries all available evaluation
     1.9 +  techniques and prints the result of the first succeeding one, unless a particular
    1.10 +  technique is specified in square brackets.
    1.11 +
    1.12    Static evaluation freezes the code generator configuration at a
    1.13    certain point and uses this context whenever evaluation is issued
    1.14    later on.  This is particularly appropriate for proof procedures
     2.1 --- a/doc-src/Codegen/Thy/document/Evaluation.tex	Sun Jul 03 08:15:14 2011 +0200
     2.2 +++ b/doc-src/Codegen/Thy/document/Evaluation.tex	Sun Jul 03 09:59:25 2011 +0200
     2.3 @@ -152,7 +152,12 @@
     2.4  \endisadelimquote
     2.5  %
     2.6  \begin{isamarkuptext}%
     2.7 -Static evaluation freezes the code generator configuration at a
     2.8 +To employ dynamic evaluation in the document generation, there is also
     2.9 +  a \isa{value} antiquotation. By default, it also tries all available evaluation
    2.10 +  techniques and prints the result of the first succeeding one, unless a particular
    2.11 +  technique is specified in square brackets.
    2.12 +
    2.13 +  Static evaluation freezes the code generator configuration at a
    2.14    certain point and uses this context whenever evaluation is issued
    2.15    later on.  This is particularly appropriate for proof procedures
    2.16    which use evaluation, since then the behaviour of evaluation is not