
%% $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: 
