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