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