doc-src/Codegen/codegen.tex
changeset 38629 eccccdeb3f73
parent 37613 355ec1b521e6
child 38631 7935b334893e
     1.1 --- a/doc-src/Codegen/codegen.tex	Fri Aug 13 13:43:54 2010 +0200
     1.2 +++ b/doc-src/Codegen/codegen.tex	Fri Aug 13 13:43:55 2010 +0200
     1.3 @@ -20,9 +20,9 @@
     1.4  \maketitle
     1.5  
     1.6  \begin{abstract}
     1.7 -  \noindent This tutorial gives an introduction to a generic code generator framework in Isabelle
     1.8 -  for generating executable code in functional programming languages from logical
     1.9 -  specifications in Isabelle/HOL.
    1.10 +  \noindent This tutorial introduces the code generator facilities of Isabelle/HOL.
    1.11 +    They empower the user to turn HOL specifications into corresponding executable
    1.12 +    programs in the languages SML, OCaml and Haskell.
    1.13  \end{abstract}
    1.14  
    1.15  \thispagestyle{empty}\clearpage