
diff -r 58fc3a3af71f -r eccccdeb3f73 doc-src/Codegen/codegen.tex
--- 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




