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