1.1 --- a/doc-src/IsarAdvanced/Codegen/codegen.tex	Wed Mar 04 11:05:02 2009 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,53 +0,0 @@
     1.4 -
     1.5 -\documentclass[12pt,a4paper,fleqn]{report}
     1.6 -\usepackage{latexsym,graphicx}
     1.7 -\usepackage[refpage]{nomencl}
     1.8 -\usepackage{../../iman,../../extra,../../isar,../../proof}
     1.9 -\usepackage{../../isabelle,../../isabellesym}
    1.10 -\usepackage{style}
    1.11 -\usepackage{pgf}
    1.12 -\usepackage{pgflibraryshapes}
    1.13 -\usepackage{tikz}
    1.14 -\usepackage{../../pdfsetup}
    1.15 -
    1.16 -\hyphenation{Isabelle}
    1.17 -\hyphenation{Isar}
    1.18 -\isadroptag{theory}
    1.19 -
    1.20 -\title{\includegraphics[scale=0.5]{isabelle_isar}
    1.21 -  \\[4ex] Code generation from Isabelle/HOL theories}
    1.22 -\author{\emph{Florian Haftmann}}
    1.23 -
    1.24 -\begin{document}
    1.25 -
    1.26 -\maketitle
    1.27 -
    1.28 -\begin{abstract}
    1.29 -  This tutorial gives an introduction to a generic code generator framework in Isabelle
    1.30 -  for generating executable code in functional programming languages from logical
    1.31 -  specifications in Isabelle/HOL.
    1.32 -\end{abstract}
    1.33 -
    1.34 -\thispagestyle{empty}\clearpage
    1.35 -
    1.36 -\pagenumbering{roman}
    1.37 -\clearfirst
    1.38 -
    1.39 -\input{Thy/document/Introduction.tex}
    1.40 -\input{Thy/document/Program.tex}
    1.41 -\input{Thy/document/Adaption.tex}
    1.42 -\input{Thy/document/Further.tex}
    1.43 -\input{Thy/document/ML.tex}
    1.44 -
    1.45 -\begingroup
    1.46 -\bibliographystyle{plain} \small\raggedright\frenchspacing
    1.47 -\bibliography{../../manual}
    1.48 -\endgroup
    1.49 -
    1.50 -\end{document}
    1.51 -
    1.52 -
    1.53 -%%% Local Variables: 
    1.54 -%%% mode: latex
    1.55 -%%% TeX-master: t
    1.56 -%%% End: