doc-src/Codegen/codegen.tex
author wenzelm
Wed, 15 Apr 2009 11:14:48 +0200
changeset 30895 bad26d8f0adf
parent 30836 1344132160bb
child 31050 555b56b66fcf
permissions -rw-r--r--
updated for Isabelle2009;
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}
30226
2f4684e2ea95 more canonical directory structure of manuals
haftmann
parents: 29017
diff changeset
     5
\usepackage{../iman,../extra,../isar,../proof}
2f4684e2ea95 more canonical directory structure of manuals
haftmann
parents: 29017
diff changeset
     6
\usepackage{../isabelle,../isabellesym}
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
     7
\usepackage{style}
30226
2f4684e2ea95 more canonical directory structure of manuals
haftmann
parents: 29017
diff changeset
     8
\usepackage{../pdfsetup}
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
     9
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    10
\hyphenation{Isabelle}
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    11
\hyphenation{Isar}
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    12
\isadroptag{theory}
28564
haftmann
parents: 28560
diff changeset
    13
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    14
\title{\includegraphics[scale=0.5]{isabelle_isar}
21222
6dfdb69e83ef adjusted title
haftmann
parents: 21190
diff changeset
    15
  \\[4ex] Code generation from Isabelle/HOL theories}
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    16
\author{\emph{Florian Haftmann}}
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    17
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    18
\begin{document}
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    19
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    20
\maketitle
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    21
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    22
\begin{abstract}
30227
853abb4853cc tuned manuals
haftmann
parents: 30226
diff changeset
    23
  \noindent This tutorial gives an introduction to a generic code generator framework in Isabelle
28213
b52f9205a02d New outline for codegen tutorial -- draft
haftmann
parents: 26911
diff changeset
    24
  for generating executable code in functional programming languages from logical
b52f9205a02d New outline for codegen tutorial -- draft
haftmann
parents: 26911
diff changeset
    25
  specifications in Isabelle/HOL.
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    26
\end{abstract}
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    27
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    28
\thispagestyle{empty}\clearpage
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    29
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    30
\pagenumbering{roman}
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    31
\clearfirst
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    32
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
    33
\input{Thy/document/Introduction.tex}
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
    34
\input{Thy/document/Program.tex}
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
    35
\input{Thy/document/Adaption.tex}
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
    36
\input{Thy/document/Further.tex}
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
    37
\input{Thy/document/ML.tex}
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    38
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    39
\begingroup
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    40
\bibliographystyle{plain} \small\raggedright\frenchspacing
30226
2f4684e2ea95 more canonical directory structure of manuals
haftmann
parents: 29017
diff changeset
    41
\bibliography{../manual}
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    42
\endgroup
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    43
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    44
\end{document}
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    45
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    46
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    47
%%% Local Variables: 
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    48
%%% mode: latex
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    49
%%% TeX-master: t
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    50
%%% End: