added evaluation section
authorhaftmann
Sat, 27 Nov 2010 18:51:04 +0100
changeset 409915288144b4358
parent 40990 aae9a020fa77
child 40992 e3d4f2522a5f
added evaluation section
doc-src/Codegen/Thy/Introduction.thy
     1.1 --- a/doc-src/Codegen/Thy/Introduction.thy	Sat Nov 27 18:51:04 2010 +0100
     1.2 +++ b/doc-src/Codegen/Thy/Introduction.thy	Sat Nov 27 18:51:04 2010 +0100
     1.3 @@ -214,6 +214,10 @@
     1.4      \item Inductive predicates can be turned executable using an
     1.5        extension of the code generator \secref{sec:inductive}.
     1.6  
     1.7 +    \item If you want to utilize code generation to obtain fast
     1.8 +      evaluators e.g.~for decision procedures, have a look at
     1.9 +      \secref{sec:evaluation}.
    1.10 +
    1.11      \item You may want to skim over the more technical sections
    1.12        \secref{sec:adaptation} and \secref{sec:further}.
    1.13