# HG changeset patch
# User haftmann
# Date 1547490828 0
# Node ID 7357a4f79f60fa482782f24482c6052543107ef1
# Parent  48bf42e7c73b283688538c12db7c7f8d4ff903f1
tuned language

diff -r 48bf42e7c73b -r 7357a4f79f60 src/Doc/Codegen/Evaluation.thy
--- a/src/Doc/Codegen/Evaluation.thy	Mon Jan 14 16:47:29 2019 +0100
+++ b/src/Doc/Codegen/Evaluation.thy	Mon Jan 14 18:33:48 2019 +0000
@@ -197,7 +197,7 @@
   code performing static evaluation (called a \<^emph>\<open>computation\<close>)
   is compiled once and for all such that later calls do not
   require any invocation of the code generator or the ML
-  compiler at all.  This topic deserved a dedicated chapter
+  compiler at all.  This topic deserves a dedicated chapter
   \secref{sec:computations}.
 \<close>