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