--- a/doc-src/IsarAdvanced/Codegen/codegen.tex Fri Sep 12 12:04:20 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/codegen.tex Sun Sep 14 21:50:35 2008 +0200
@@ -80,10 +80,9 @@
\maketitle
\begin{abstract}
- This tutorial gives a motivation-driven introduction
- to a generic code generator framework in Isabelle
- for generating executable code in functional
- programming languages from logical specifications.
+ This tutorial gives am introduction to a generic code generator framework in Isabelle
+ for generating executable code in functional programming languages from logical
+ specifications in Isabelle/HOL.
\end{abstract}
\thispagestyle{empty}\clearpage
@@ -92,6 +91,11 @@
\clearfirst
\input{Thy/document/Codegen.tex}
+% \input{Thy/document/Introduction.tex}
+% \input{Thy/document/Program.tex}
+% \input{Thy/document/Adaption.tex}
+% \input{Thy/document/Further.tex}
+% \input{Thy/document/ML.tex}
\begingroup
%\tocentry{\bibname}