4 \documentclass[12pt,a4paper,fleqn]{report}
5 \usepackage{latexsym,graphicx}
7 \usepackage[refpage]{nomencl}
8 \usepackage{../../iman,../../extra,../../isar,../../proof}
9 \usepackage{../../isabelle,../../isabellesym}
11 \usepackage{../../pdfsetup}
13 \newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
18 \newenvironment{quoteme}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
19 \renewcommand{\isatagquoteme}{\begin{quoteme}}
20 \renewcommand{\endisatagquoteme}{\end{quoteme}}
23 \renewcommand{\isatagtt}{\begin{quoteme}\isabellestyle{tt}\isastyle}
24 \renewcommand{\endisatagtt}{\end{quoteme}\isabellestyle{it}\isastyle}
28 \newcommand{\isactrlbvec}{\emph\bgroup\begin{math}{}\overline\bgroup\mbox\bgroup\isastylescript}
29 \newcommand{\isactrlevec}{\egroup\egroup\end{math}\egroup}
31 \newcommand{\qt}[1]{``#1''}
32 \newcommand{\qtt}[1]{"{}{#1}"{}}
33 \newcommand{\qn}[1]{\emph{#1}}
34 \newcommand{\strong}[1]{{\bfseries #1}}
35 \newcommand{\fixme}[1][!]{\strong{FIXME: #1}}
37 \hyphenation{Isabelle}
41 \title{\includegraphics[scale=0.5]{isabelle_isar}
42 \\[4ex] Code generation from Isabelle/HOL theories}
43 \author{\emph{Florian Haftmann}}
51 This tutorial gives am introduction to a generic code generator framework in Isabelle
52 for generating executable code in functional programming languages from logical
53 specifications in Isabelle/HOL.
56 \thispagestyle{empty}\clearpage
61 \input{Thy/document/Introduction.tex}
62 \input{Thy/document/Program.tex}
63 \input{Thy/document/Adaption.tex}
64 \input{Thy/document/Further.tex}
65 \input{Thy/document/ML.tex}
69 \bibliographystyle{plain} \small\raggedright\frenchspacing
70 \bibliography{../../manual}