doc-src/Codegen/codegen.tex
author hoelzl
Wed, 23 Feb 2011 11:33:45 +0100
changeset 41830 719b0a517c33
parent 39693 2ef15ec8e7dc
child 42511 bf89455ccf9d
permissions -rw-r--r--
log is borel measurable
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
     1
30227
853abb4853cc tuned manuals
haftmann
parents: 30226
diff changeset
     2
\documentclass[12pt,a4paper,fleqn]{article}
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
     3
\usepackage{latexsym,graphicx}
9b9910b82645 initial draft
haftmann
parents:
diff changeset
     4
\usepackage[refpage]{nomencl}
39693
2ef15ec8e7dc tuned schema table
haftmann
parents: 38813
diff changeset
     5
\usepackage{multirow}
30226
2f4684e2ea95 more canonical directory structure of manuals
haftmann
parents: 29017
diff changeset
     6
\usepackage{../iman,../extra,../isar,../proof}
2f4684e2ea95 more canonical directory structure of manuals
haftmann
parents: 29017
diff changeset
     7
\usepackage{../isabelle,../isabellesym}
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
     8
\usepackage{style}
30226
2f4684e2ea95 more canonical directory structure of manuals
haftmann
parents: 29017
diff changeset
     9
\usepackage{../pdfsetup}
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    10
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    11
\hyphenation{Isabelle}
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    12
\hyphenation{Isar}
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    13
\isadroptag{theory}
28564
haftmann
parents: 28560
diff changeset
    14
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    15
\title{\includegraphics[scale=0.5]{isabelle_isar}
21222
6dfdb69e83ef adjusted title
haftmann
parents: 21190
diff changeset
    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
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    18
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    19
\begin{document}
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    20
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    21
\maketitle
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    22
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    23
\begin{abstract}
38403
eccccdeb3f73 refined abstract
haftmann
parents: 37613
diff changeset
    24
  \noindent This tutorial introduces the code generator facilities of Isabelle/HOL.
eccccdeb3f73 refined abstract
haftmann
parents: 37613
diff changeset
    25
    They empower the user to turn HOL specifications into corresponding executable
38813
f50f0802ba99 updated generated files
haftmann
parents: 38510
diff changeset
    26
    programs in the languages SML, OCaml, Haskell and Scala.
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    27
\end{abstract}
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    28
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    29
\thispagestyle{empty}\clearpage
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    30
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    31
\pagenumbering{roman}
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    32
\clearfirst
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    33
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
    34
\input{Thy/document/Introduction.tex}
38405
7935b334893e sketch of new outline
haftmann
parents: 38403
diff changeset
    35
\input{Thy/document/Foundations.tex}
7935b334893e sketch of new outline
haftmann
parents: 38403
diff changeset
    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
555b56b66fcf adaptation replaces adaption
haftmann
parents: 30836
diff changeset
    38
\input{Thy/document/Adaptation.tex}
38510
ec0408c7328b stub for evaluation chapter
haftmann
parents: 38405
diff changeset
    39
\input{Thy/document/Evaluation.tex}
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
    40
\input{Thy/document/Further.tex}
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    41
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    42
\begingroup
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    43
\bibliographystyle{plain} \small\raggedright\frenchspacing
30226
2f4684e2ea95 more canonical directory structure of manuals
haftmann
parents: 29017
diff changeset
    44
\bibliography{../manual}
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    45
\endgroup
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    46
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    47
\end{document}
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    48
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    49
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    50
%%% Local Variables: 
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    51
%%% mode: latex
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    52
%%% TeX-master: t
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    53
%%% End: