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