src/Doc/Codegen/Evaluation.thy
changeset 58620 7435b6a3f72e
parent 58310 91ea607a34d8
child 59334 f0141b991c8f
     1.1 --- a/src/Doc/Codegen/Evaluation.thy	Tue Oct 07 21:44:41 2014 +0200
     1.2 +++ b/src/Doc/Codegen/Evaluation.thy	Tue Oct 07 22:35:11 2014 +0200
     1.3 @@ -53,7 +53,7 @@
     1.4  subsubsection {* Normalization by evaluation (@{text nbe}) *}
     1.5  
     1.6  text {*
     1.7 -  Normalization by evaluation \cite{Aehlig-Haftmann-Nipkow:2008:nbe}
     1.8 +  Normalization by evaluation @{cite "Aehlig-Haftmann-Nipkow:2008:nbe"}
     1.9    provides a comparably fast partially symbolic evaluation which
    1.10    permits also normalization of functions and uninterpreted symbols;
    1.11    the stack of code to be trusted is considerable.