1
2\documentclass[12pt,a4paper,fleqn]{article}
3\usepackage[T1]{fontenc}
4\usepackage{latexsym,graphicx}
5\usepackage{tikz}\usetikzlibrary{shapes}\usetikzlibrary{arrows}
6\usepackage{multirow}
7\usepackage{iman,extra,isar}
8\usepackage{isabelle,isabellesym}
9\usepackage{style}
10\usepackage{pdfsetup}
11
12\hyphenation{Isabelle}
13\hyphenation{Isar}
14\isadroptag{theory}
15
16\title{\includegraphics[scale=0.5]{isabelle_isar}
17  \\[4ex] Code generation from Isabelle/HOL theories}
18\author{\emph{Florian Haftmann with contributions from Lukas Bulwahn}}
19
20\begin{document}
21
22\maketitle
23
24\begin{abstract}
25  \noindent This tutorial introduces the code generator facilities of Isabelle/HOL.
26    They empower the user to turn HOL specifications into corresponding executable
27    programs in the languages SML, OCaml, Haskell and Scala.
28\end{abstract}
29
30\thispagestyle{empty}\clearpage
31
32\pagenumbering{roman}
33\clearfirst
34
35\input{Introduction.tex}
36\input{Foundations.tex}
37\input{Refinement.tex}
38\input{Inductive_Predicate.tex}
39\input{Evaluation.tex}
40\input{Computations.tex}
41\input{Adaptation.tex}
42\input{Further.tex}
43
44\begingroup
45\bibliographystyle{plain} \small\raggedright\frenchspacing
46\bibliography{manual}
47\endgroup
48
49\end{document}
50
51
52%%% Local Variables: 
53%%% mode: latex
54%%% TeX-master: t
55%%% End: 
56