\documentclass[12pt,a4paper,fleqn]{article}\usepackage{latexsym,graphicx}\usepackage[refpage]{nomencl}\usepackage{../iman,../extra,../isar,../proof}\usepackage{../isabelle,../isabellesym}\usepackage{style}\usepackage{../pdfsetup}\hyphenation{Isabelle}\hyphenation{Isar}\isadroptag{theory}\title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] Code generation from Isabelle/HOL theories}\author{\emph{Florian Haftmann with contributions from Lukas Bulwahn}}\begin{document}\maketitle\begin{abstract} \noindent This tutorial introduces the code generator facilities of Isabelle/HOL. They empower the user to turn HOL specifications into corresponding executable programs in the languages SML, OCaml and Haskell.\end{abstract}\thispagestyle{empty}\clearpage\pagenumbering{roman}\clearfirst\input{Thy/document/Introduction.tex}\input{Thy/document/Foundations.tex}\input{Thy/document/Refinement.tex}\input{Thy/document/Inductive_Predicate.tex}\input{Thy/document/Adaptation.tex}\input{Thy/document/Evaluation.tex}\input{Thy/document/Further.tex}\begingroup\bibliographystyle{plain} \small\raggedright\frenchspacing\bibliography{../manual}\endgroup\end{document}%%% Local Variables: %%% mode: latex%%% TeX-master: t%%% End: