%% $Id$
\documentclass[12pt,a4paper,fleqn]{report}
\usepackage{latexsym,graphicx}
\usepackage{listings}
\usepackage[refpage]{nomencl}
\usepackage{../../iman,../../extra,../../isar,../../proof}
\usepackage{../../isabelle,../../isabellesym}
\usepackage{style}
\usepackage{../../pdfsetup}
\newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
\makeatletter
\isakeeptag{quoteme}
\newenvironment{quoteme}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
\renewcommand{\isatagquoteme}{\begin{quoteme}}
\renewcommand{\endisatagquoteme}{\end{quoteme}}
\isakeeptag{tt}
\renewcommand{\isatagtt}{\begin{quoteme}\isabellestyle{tt}\isastyle}
\renewcommand{\endisatagtt}{\end{quoteme}\isabellestyle{it}\isastyle}
\makeatother
\newcommand{\isactrlbvec}{\emph\bgroup\begin{math}{}\overline\bgroup\mbox\bgroup\isastylescript}
\newcommand{\isactrlevec}{\egroup\egroup\end{math}\egroup}
\newcommand{\qt}[1]{``#1''}
\newcommand{\qtt}[1]{"{}{#1}"{}}
\newcommand{\qn}[1]{\emph{#1}}
\newcommand{\strong}[1]{{\bfseries #1}}
\newcommand{\fixme}[1][!]{\strong{FIXME: #1}}
\hyphenation{Isabelle}
\hyphenation{Isar}
\isadroptag{theory}
\title{\includegraphics[scale=0.5]{isabelle_isar}
\\[4ex] Code generation from Isabelle/HOL theories}
\author{\emph{Florian Haftmann}}
\begin{document}
\maketitle
\begin{abstract}
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.
\end{abstract}
\thispagestyle{empty}\clearpage
\pagenumbering{roman}
\clearfirst
\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}
\bibliographystyle{plain} \small\raggedright\frenchspacing
\bibliography{../../manual}
\endgroup
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: