equal
deleted
inserted
replaced
1 |
|
2 \documentclass[12pt,a4paper,fleqn]{report} |
|
3 \usepackage{latexsym,graphicx} |
|
4 \usepackage[refpage]{nomencl} |
|
5 \usepackage{../../iman,../../extra,../../isar,../../proof} |
|
6 \usepackage{../../isabelle,../../isabellesym} |
|
7 \usepackage{style} |
|
8 \usepackage{pgf} |
|
9 \usepackage{pgflibraryshapes} |
|
10 \usepackage{tikz} |
|
11 \usepackage{../../pdfsetup} |
|
12 |
|
13 \hyphenation{Isabelle} |
|
14 \hyphenation{Isar} |
|
15 \isadroptag{theory} |
|
16 |
|
17 \title{\includegraphics[scale=0.5]{isabelle_isar} |
|
18 \\[4ex] Code generation from Isabelle/HOL theories} |
|
19 \author{\emph{Florian Haftmann}} |
|
20 |
|
21 \begin{document} |
|
22 |
|
23 \maketitle |
|
24 |
|
25 \begin{abstract} |
|
26 This tutorial gives an introduction to a generic code generator framework in Isabelle |
|
27 for generating executable code in functional programming languages from logical |
|
28 specifications in Isabelle/HOL. |
|
29 \end{abstract} |
|
30 |
|
31 \thispagestyle{empty}\clearpage |
|
32 |
|
33 \pagenumbering{roman} |
|
34 \clearfirst |
|
35 |
|
36 \input{Thy/document/Introduction.tex} |
|
37 \input{Thy/document/Program.tex} |
|
38 \input{Thy/document/Adaption.tex} |
|
39 \input{Thy/document/Further.tex} |
|
40 \input{Thy/document/ML.tex} |
|
41 |
|
42 \begingroup |
|
43 \bibliographystyle{plain} \small\raggedright\frenchspacing |
|
44 \bibliography{../../manual} |
|
45 \endgroup |
|
46 |
|
47 \end{document} |
|
48 |
|
49 |
|
50 %%% Local Variables: |
|
51 %%% mode: latex |
|
52 %%% TeX-master: t |
|
53 %%% End: |
|