# HG changeset patch
# User haftmann
# Date 1290880264 -3600
# Node ID 5288144b43582aea55fa4281f931bba886e2959e
# Parent  aae9a020fa770b2c418643f789c212965242b772
added evaluation section

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}.