doc-src/Codegen/Thy/Introduction.thy
changeset 40753 5288144b4358
parent 39745 3aa2bc9c5478
child 42096 9f6652122963
--- 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}.