doc-src/Codegen/codegen.tex
author haftmann
Fri Jan 22 13:38:28 2010 +0100 (2010-01-22)
changeset 34944 970e1466028d
parent 33926 dd017d9db05f
child 37613 355ec1b521e6
permissions -rw-r--r--
code literals: distinguish numeral classes by different entries
     1 
     2 \documentclass[12pt,a4paper,fleqn]{article}
     3 \usepackage{latexsym,graphicx}
     4 \usepackage[refpage]{nomencl}
     5 \usepackage{../iman,../extra,../isar,../proof}
     6 \usepackage{../isabelle,../isabellesym}
     7 \usepackage{style}
     8 \usepackage{../pdfsetup}
     9 
    10 \hyphenation{Isabelle}
    11 \hyphenation{Isar}
    12 \isadroptag{theory}
    13 
    14 \title{\includegraphics[scale=0.5]{isabelle_isar}
    15   \\[4ex] Code generation from Isabelle/HOL theories}
    16 \author{\emph{Florian Haftmann with contributions from Lukas Bulwahn}}
    17 
    18 \begin{document}
    19 
    20 \maketitle
    21 
    22 \begin{abstract}
    23   \noindent This tutorial gives an introduction to a generic code generator framework in Isabelle
    24   for generating executable code in functional programming languages from logical
    25   specifications in Isabelle/HOL.
    26 \end{abstract}
    27 
    28 \thispagestyle{empty}\clearpage
    29 
    30 \pagenumbering{roman}
    31 \clearfirst
    32 
    33 \input{Thy/document/Introduction.tex}
    34 \input{Thy/document/Program.tex}
    35 \input{Thy/document/Adaptation.tex}
    36 \input{Thy/document/Further.tex}
    37 \input{Thy/document/ML.tex}
    38 
    39 \begingroup
    40 \bibliographystyle{plain} \small\raggedright\frenchspacing
    41 \bibliography{../manual}
    42 \endgroup
    43 
    44 \end{document}
    45 
    46 
    47 %%% Local Variables: 
    48 %%% mode: latex
    49 %%% TeX-master: t
    50 %%% End: