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;
     1 
     2 \documentclass[12pt,a4paper,fleqn]{article}
     3 \usepackage{latexsym,graphicx}
     4 \usepackage[refpage]{nomencl}
     5 \usepackage{multirow}
     6 \usepackage{../iman,../extra,../isar,../proof}
     7 \usepackage{../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
     8 \usepackage{style}
     9 \usepackage{../pdfsetup}
    10 
    11 \hyphenation{Isabelle}
    12 \hyphenation{Isar}
    13 \isadroptag{theory}
    14 
    15 \title{\includegraphics[scale=0.5]{isabelle_isar}
    16   \\[4ex] Code generation from Isabelle/HOL theories}
    17 \author{\emph{Florian Haftmann with contributions from Lukas Bulwahn}}
    18 
    19 \begin{document}
    20 
    21 \maketitle
    22 
    23 \begin{abstract}
    24   \noindent This tutorial introduces the code generator facilities of Isabelle/HOL.
    25     They empower the user to turn HOL specifications into corresponding executable
    26     programs in the languages SML, OCaml, Haskell and Scala.
    27 \end{abstract}
    28 
    29 \thispagestyle{empty}\clearpage
    30 
    31 \pagenumbering{roman}
    32 \clearfirst
    33 
    34 \input{Thy/document/Introduction.tex}
    35 \input{Thy/document/Foundations.tex}
    36 \input{Thy/document/Refinement.tex}
    37 \input{Thy/document/Inductive_Predicate.tex}
    38 \input{Thy/document/Adaptation.tex}
    39 \input{Thy/document/Evaluation.tex}
    40 \input{Thy/document/Further.tex}
    41 
    42 \begingroup
    43 \bibliographystyle{plain} \small\raggedright\frenchspacing
    44 \bibliography{../manual}
    45 \endgroup
    46 
    47 \end{document}
    48 
    49 
    50 %%% Local Variables: 
    51 %%% mode: latex
    52 %%% TeX-master: t
    53 %%% End: