author | wenzelm |
Tue, 18 May 2021 15:17:55 +0200 | |
changeset 73723 | 1bbbaae6b5e3 |
parent 73401 | 8b464825d2b5 |
child 76649 | 9a6cb5ecc183 |
permissions | -rw-r--r-- |
20948 | 1 |
|
30227 | 2 |
\documentclass[12pt,a4paper,fleqn]{article} |
70010
499896e3a7b0
clarified style: allow to search PDF for keywords containing "_";
wenzelm
parents:
65041
diff
changeset
|
3 |
\usepackage[T1]{fontenc} |
73401 | 4 |
\usepackage{graphicx} |
52742 | 5 |
\usepackage{tikz}\usetikzlibrary{shapes}\usetikzlibrary{arrows} |
39693 | 6 |
\usepackage{multirow} |
50426
d2c60ada3ece
eliminated old copy of proof.sty (1995), prefer the one usually included in current latex distributions (2005);
wenzelm
parents:
48985
diff
changeset
|
7 |
\usepackage{iman,extra,isar} |
48951
b9238cbcdd41
more standard document preparation within session context;
wenzelm
parents:
42511
diff
changeset
|
8 |
\usepackage{isabelle,isabellesym} |
20948 | 9 |
\usepackage{style} |
48951
b9238cbcdd41
more standard document preparation within session context;
wenzelm
parents:
42511
diff
changeset
|
10 |
\usepackage{pdfsetup} |
20948 | 11 |
|
12 |
\hyphenation{Isabelle} |
|
13 |
\hyphenation{Isar} |
|
14 |
\isadroptag{theory} |
|
28564 | 15 |
|
73723 | 16 |
\title{\includegraphics[scale=0.5]{isabelle_logo} |
21222 | 17 |
\\[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
|
18 |
\author{\emph{Florian Haftmann with contributions from Lukas Bulwahn}} |
20948 | 19 |
|
20 |
\begin{document} |
|
21 |
||
22 |
\maketitle |
|
23 |
||
24 |
\begin{abstract} |
|
38403 | 25 |
\noindent This tutorial introduces the code generator facilities of Isabelle/HOL. |
26 |
They empower the user to turn HOL specifications into corresponding executable |
|
38813 | 27 |
programs in the languages SML, OCaml, Haskell and Scala. |
20948 | 28 |
\end{abstract} |
29 |
||
30 |
\thispagestyle{empty}\clearpage |
|
31 |
||
32 |
\pagenumbering{roman} |
|
33 |
\clearfirst |
|
34 |
||
48951
b9238cbcdd41
more standard document preparation within session context;
wenzelm
parents:
42511
diff
changeset
|
35 |
\input{Introduction.tex} |
b9238cbcdd41
more standard document preparation within session context;
wenzelm
parents:
42511
diff
changeset
|
36 |
\input{Foundations.tex} |
b9238cbcdd41
more standard document preparation within session context;
wenzelm
parents:
42511
diff
changeset
|
37 |
\input{Refinement.tex} |
b9238cbcdd41
more standard document preparation within session context;
wenzelm
parents:
42511
diff
changeset
|
38 |
\input{Inductive_Predicate.tex} |
61780
b319013d2d33
moved section according to supposed order of interest
haftmann
parents:
52742
diff
changeset
|
39 |
\input{Evaluation.tex} |
65041 | 40 |
\input{Computations.tex} |
48951
b9238cbcdd41
more standard document preparation within session context;
wenzelm
parents:
42511
diff
changeset
|
41 |
\input{Adaptation.tex} |
b9238cbcdd41
more standard document preparation within session context;
wenzelm
parents:
42511
diff
changeset
|
42 |
\input{Further.tex} |
20948 | 43 |
|
44 |
\begingroup |
|
45 |
\bibliographystyle{plain} \small\raggedright\frenchspacing |
|
48951
b9238cbcdd41
more standard document preparation within session context;
wenzelm
parents:
42511
diff
changeset
|
46 |
\bibliography{manual} |
20948 | 47 |
\endgroup |
48 |
||
49 |
\end{document} |
|
50 |
||
51 |
||
52 |
%%% Local Variables: |
|
53 |
%%% mode: latex |
|
54 |
%%% TeX-master: t |
|
55 |
%%% End: |