author | hoelzl |
Wed, 23 Feb 2011 11:33:45 +0100 | |
changeset 41830 | 719b0a517c33 |
parent 39693 | 2ef15ec8e7dc |
child 42511 | bf89455ccf9d |
permissions | -rw-r--r-- |
20948 | 1 |
|
30227 | 2 |
\documentclass[12pt,a4paper,fleqn]{article} |
20948 | 3 |
\usepackage{latexsym,graphicx} |
4 |
\usepackage[refpage]{nomencl} |
|
39693 | 5 |
\usepackage{multirow} |
30226 | 6 |
\usepackage{../iman,../extra,../isar,../proof} |
7 |
\usepackage{../isabelle,../isabellesym} |
|
20948 | 8 |
\usepackage{style} |
30226 | 9 |
\usepackage{../pdfsetup} |
20948 | 10 |
|
11 |
\hyphenation{Isabelle} |
|
12 |
\hyphenation{Isar} |
|
13 |
\isadroptag{theory} |
|
28564 | 14 |
|
20948 | 15 |
\title{\includegraphics[scale=0.5]{isabelle_isar} |
21222 | 16 |
\\[4ex] Code generation from Isabelle/HOL theories} |
33926
dd017d9db05f
adding subsection about the predicate compiler to the code generator tutorial
bulwahn
parents:
31050
diff
changeset
|
17 |
\author{\emph{Florian Haftmann with contributions from Lukas Bulwahn}} |
20948 | 18 |
|
19 |
\begin{document} |
|
20 |
||
21 |
\maketitle |
|
22 |
||
23 |
\begin{abstract} |
|
38403 | 24 |
\noindent This tutorial introduces the code generator facilities of Isabelle/HOL. |
25 |
They empower the user to turn HOL specifications into corresponding executable |
|
38813 | 26 |
programs in the languages SML, OCaml, Haskell and Scala. |
20948 | 27 |
\end{abstract} |
28 |
||
29 |
\thispagestyle{empty}\clearpage |
|
30 |
||
31 |
\pagenumbering{roman} |
|
32 |
\clearfirst |
|
33 |
||
28419 | 34 |
\input{Thy/document/Introduction.tex} |
38405 | 35 |
\input{Thy/document/Foundations.tex} |
36 |
\input{Thy/document/Refinement.tex} |
|
37613
355ec1b521e6
split off predicate compiler into separate theory
haftmann
parents:
33926
diff
changeset
|
37 |
\input{Thy/document/Inductive_Predicate.tex} |
31050 | 38 |
\input{Thy/document/Adaptation.tex} |
38510 | 39 |
\input{Thy/document/Evaluation.tex} |
28419 | 40 |
\input{Thy/document/Further.tex} |
20948 | 41 |
|
42 |
\begingroup |
|
43 |
\bibliographystyle{plain} \small\raggedright\frenchspacing |
|
30226 | 44 |
\bibliography{../manual} |
20948 | 45 |
\endgroup |
46 |
||
47 |
\end{document} |
|
48 |
||
49 |
||
50 |
%%% Local Variables: |
|
51 |
%%% mode: latex |
|
52 |
%%% TeX-master: t |
|
53 |
%%% End: |