src/Doc/Codegen/Evaluation.thy
changeset 69658 7357a4f79f60
parent 69597 ff784d5a5bfb
child 72375 e48d93811ed7
equal deleted inserted replaced
69657:48bf42e7c73b 69658:7357a4f79f60
   195   the required generated code is inserted directly into an ML
   195   the required generated code is inserted directly into an ML
   196   block using antiquotations.  The idea is that generated
   196   block using antiquotations.  The idea is that generated
   197   code performing static evaluation (called a \<^emph>\<open>computation\<close>)
   197   code performing static evaluation (called a \<^emph>\<open>computation\<close>)
   198   is compiled once and for all such that later calls do not
   198   is compiled once and for all such that later calls do not
   199   require any invocation of the code generator or the ML
   199   require any invocation of the code generator or the ML
   200   compiler at all.  This topic deserved a dedicated chapter
   200   compiler at all.  This topic deserves a dedicated chapter
   201   \secref{sec:computations}.
   201   \secref{sec:computations}.
   202 \<close>
   202 \<close>
   203   
   203   
   204 end
   204 end