wneuper/isa: doc-src/IsarAdvanced/Codegen/codegen.tex@9a1eaad4a7bb

     2 \documentclass[12pt,a4paper,fleqn]{report}

     3 \usepackage{latexsym,graphicx}

     4 \usepackage[refpage]{nomencl}

     5 \usepackage{../../iman,../../extra,../../isar,../../proof}

     6 \usepackage{../../isabelle,../../isabellesym}

     7 \usepackage{style}

     8 \usepackage{pgf}

     9 \usepackage{pgflibraryshapes}

    10 \usepackage{tikz}

    11 \usepackage{../../pdfsetup}

    13 \hyphenation{Isabelle}

    14 \hyphenation{Isar}

    15 \isadroptag{theory}

    17 \title{\includegraphics[scale=0.5]{isabelle_isar}

    18   \\[4ex] Code generation from Isabelle/HOL theories}

    19 \author{\emph{Florian Haftmann}}

    21 \begin{document}

    23 \maketitle

    25 \begin{abstract}

    26   This tutorial gives an introduction to a generic code generator framework in Isabelle

    27   for generating executable code in functional programming languages from logical

    28   specifications in Isabelle/HOL.

    29 \end{abstract}

    31 \thispagestyle{empty}\clearpage

    33 \pagenumbering{roman}

    34 \clearfirst

    36 \input{Thy/document/Introduction.tex}

    37 \input{Thy/document/Program.tex}

    38 \input{Thy/document/Adaption.tex}

    39 \input{Thy/document/Further.tex}

    40 \input{Thy/document/ML.tex}

    42 \begingroup

    43 \bibliographystyle{plain} \small\raggedright\frenchspacing

    44 \bibliography{../../manual}

    45 \endgroup

    47 \end{document}

    50 %%% Local Variables:

    51 %%% mode: latex

    52 %%% TeX-master: t

    53 %%% End:

author	haftmann
	Mon, 08 Dec 2008 10:27:40 +0100
changeset 29017	9a1eaad4a7bb
parent 28727	185110a4b97a
permissions	-rw-r--r--