2 \documentclass[12pt,a4paper,fleqn]{article}
3 \usepackage{latexsym,graphicx}
4 \usepackage[refpage]{nomencl}
5 \usepackage{../iman,../extra,../isar,../proof}
6 \usepackage{../isabelle,../isabellesym}
8 \usepackage{../pdfsetup}
10 \hyphenation{Isabelle}
14 \title{\includegraphics[scale=0.5]{isabelle_isar}
15 \\[4ex] Code generation from Isabelle/HOL theories}
16 \author{\emph{Florian Haftmann with contributions from Lukas Bulwahn}}
23 \noindent This tutorial introduces the code generator facilities of Isabelle/HOL.
24 They empower the user to turn HOL specifications into corresponding executable
25 programs in the languages SML, OCaml and Haskell.
28 \thispagestyle{empty}\clearpage
33 \input{Thy/document/Introduction.tex}
34 \input{Thy/document/Program.tex}
35 \input{Thy/document/Inductive_Predicate.tex}
36 \input{Thy/document/Adaptation.tex}
37 \input{Thy/document/Further.tex}
38 \input{Thy/document/ML.tex}
41 \bibliographystyle{plain} \small\raggedright\frenchspacing
42 \bibliography{../manual}