wneuper/isa: doc-src/Codegen/codegen.tex@20e3616b2d9c

     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}

    10 \hyphenation{Isabelle}

    11 \hyphenation{Isar}

    12 \isadroptag{theory}

    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}}

    18 \begin{document}

    20 \maketitle

    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}

    28 \thispagestyle{empty}\clearpage

    30 \pagenumbering{roman}

    31 \clearfirst

    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}

    39 \begingroup

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

    41 \bibliography{../manual}

    42 \endgroup

    44 \end{document}

    47 %%% Local Variables:

    48 %%% mode: latex

    49 %%% TeX-master: t

    50 %%% End:

author	Walther Neuper <neuper@ist.tugraz.at>
	Thu, 12 Aug 2010 15:03:34 +0200
branch	isac-from-Isabelle2009-2
changeset 37913	20e3616b2d9c
parent 33942	dd017d9db05f
child 37613	355ec1b521e6
permissions	-rw-r--r--