equal
deleted
inserted
replaced
|
1 |
|
2 \documentclass[12pt,a4paper,fleqn]{article} |
|
3 \usepackage{latexsym,graphicx} |
|
4 \usepackage{multirow} |
|
5 \usepackage{iman,extra,isar,proof} |
|
6 \usepackage{isabelle,isabellesym} |
|
7 \usepackage{style} |
|
8 \usepackage{pdfsetup} |
|
9 |
|
10 \hyphenation{Isabelle} |
|
11 \hyphenation{Isar} |
|
12 \isadroptag{theory} |
|
13 |
|
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}} |
|
17 |
|
18 \begin{document} |
|
19 |
|
20 \maketitle |
|
21 |
|
22 \begin{abstract} |
|
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, Haskell and Scala. |
|
26 \end{abstract} |
|
27 |
|
28 \thispagestyle{empty}\clearpage |
|
29 |
|
30 \pagenumbering{roman} |
|
31 \clearfirst |
|
32 |
|
33 \input{Introduction.tex} |
|
34 \input{Foundations.tex} |
|
35 \input{Refinement.tex} |
|
36 \input{Inductive_Predicate.tex} |
|
37 \input{Adaptation.tex} |
|
38 \input{Evaluation.tex} |
|
39 \input{Further.tex} |
|
40 |
|
41 \begingroup |
|
42 \bibliographystyle{plain} \small\raggedright\frenchspacing |
|
43 \bibliography{manual} |
|
44 \endgroup |
|
45 |
|
46 \end{document} |
|
47 |
|
48 |
|
49 %%% Local Variables: |
|
50 %%% mode: latex |
|
51 %%% TeX-master: t |
|
52 %%% End: |