equal
deleted
inserted
replaced
51 |
51 |
52 |
52 |
53 subsubsection {* Normalization by evaluation (@{text nbe}) *} |
53 subsubsection {* Normalization by evaluation (@{text nbe}) *} |
54 |
54 |
55 text {* |
55 text {* |
56 Normalization by evaluation \cite{Aehlig-Haftmann-Nipkow:2008:nbe} |
56 Normalization by evaluation @{cite "Aehlig-Haftmann-Nipkow:2008:nbe"} |
57 provides a comparably fast partially symbolic evaluation which |
57 provides a comparably fast partially symbolic evaluation which |
58 permits also normalization of functions and uninterpreted symbols; |
58 permits also normalization of functions and uninterpreted symbols; |
59 the stack of code to be trusted is considerable. |
59 the stack of code to be trusted is considerable. |
60 *} |
60 *} |
61 |
61 |