--- a/doc-src/Codegen/codegen.tex Mon Aug 27 22:31:16 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-
-\documentclass[12pt,a4paper,fleqn]{article}
-\usepackage{latexsym,graphicx}
-\usepackage[refpage]{nomencl}
-\usepackage{multirow}
-\usepackage{../iman,../extra,../isar,../proof}
-\usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
-\usepackage{style}
-\usepackage{../pdfsetup}
-
-\hyphenation{Isabelle}
-\hyphenation{Isar}
-\isadroptag{theory}
-
-\title{\includegraphics[scale=0.5]{isabelle_isar}
- \\[4ex] Code generation from Isabelle/HOL theories}
-\author{\emph{Florian Haftmann with contributions from Lukas Bulwahn}}
-
-\begin{document}
-
-\maketitle
-
-\begin{abstract}
- \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, Haskell and Scala.
-\end{abstract}
-
-\thispagestyle{empty}\clearpage
-
-\pagenumbering{roman}
-\clearfirst
-
-\input{Thy/document/Introduction.tex}
-\input{Thy/document/Foundations.tex}
-\input{Thy/document/Refinement.tex}
-\input{Thy/document/Inductive_Predicate.tex}
-\input{Thy/document/Adaptation.tex}
-\input{Thy/document/Evaluation.tex}
-\input{Thy/document/Further.tex}
-
-\begingroup
-\bibliographystyle{plain} \small\raggedright\frenchspacing
-\bibliography{../manual}
-\endgroup
-
-\end{document}
-
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End: