equal
deleted
inserted
replaced
96 *} |
96 *} |
97 |
97 |
98 value %quote [nbe] "42 / (12 :: rat)" |
98 value %quote [nbe] "42 / (12 :: rat)" |
99 |
99 |
100 text {* |
100 text {* |
|
101 To employ dynamic evaluation in the document generation, there is also |
|
102 a @{text value} antiquotation. By default, it also tries all available evaluation |
|
103 techniques and prints the result of the first succeeding one, unless a particular |
|
104 technique is specified in square brackets. |
|
105 |
101 Static evaluation freezes the code generator configuration at a |
106 Static evaluation freezes the code generator configuration at a |
102 certain point and uses this context whenever evaluation is issued |
107 certain point and uses this context whenever evaluation is issued |
103 later on. This is particularly appropriate for proof procedures |
108 later on. This is particularly appropriate for proof procedures |
104 which use evaluation, since then the behaviour of evaluation is not |
109 which use evaluation, since then the behaviour of evaluation is not |
105 changed or even compromised later on by actions of the user. |
110 changed or even compromised later on by actions of the user. |