--- a/doc-src/Codegen/codegen.tex Fri Aug 13 13:43:54 2010 +0200
+++ b/doc-src/Codegen/codegen.tex Fri Aug 13 13:43:55 2010 +0200
@@ -20,9 +20,9 @@
\maketitle
\begin{abstract}
- \noindent This tutorial gives an introduction to a generic code generator framework in Isabelle
- for generating executable code in functional programming languages from logical
- specifications in Isabelle/HOL.
+ \noindent This tutorial introduces the code generator facilities of Isabelle/HOL.
+ They empower the user to turn HOL specifications into corresponding executable
+ programs in the languages SML, OCaml and Haskell.
\end{abstract}
\thispagestyle{empty}\clearpage