diff -r aae9a020fa77 -r 5288144b4358 doc-src/Codegen/Thy/Introduction.thy --- a/doc-src/Codegen/Thy/Introduction.thy Sat Nov 27 18:51:04 2010 +0100 +++ b/doc-src/Codegen/Thy/Introduction.thy Sat Nov 27 18:51:04 2010 +0100 @@ -214,6 +214,10 @@ \item Inductive predicates can be turned executable using an extension of the code generator \secref{sec:inductive}. + \item If you want to utilize code generation to obtain fast + evaluators e.g.~for decision procedures, have a look at + \secref{sec:evaluation}. + \item You may want to skim over the more technical sections \secref{sec:adaptation} and \secref{sec:further}.