wneuper/isa: src/Doc/Codegen/document/root.tex@d2c60ada3ece

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

     3 \usepackage{latexsym,graphicx}

     4 \usepackage{multirow}

     5 \usepackage{iman,extra,isar}

     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 introduces the code generator facilities of Isabelle/HOL.

    24     They empower the user to turn HOL specifications into corresponding executable

    25     programs in the languages SML, OCaml, Haskell and Scala.

    26 \end{abstract}

    28 \thispagestyle{empty}\clearpage

    30 \pagenumbering{roman}

    31 \clearfirst

    33 \input{Introduction.tex}

    34 \input{Foundations.tex}

    35 \input{Refinement.tex}

    36 \input{Inductive_Predicate.tex}

    37 \input{Adaptation.tex}

    38 \input{Evaluation.tex}

    39 \input{Further.tex}

    41 \begingroup

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

    43 \bibliography{manual}

    44 \endgroup

    46 \end{document}

    49 %%% Local Variables:

    50 %%% mode: latex

    51 %%% TeX-master: t

    52 %%% End:

author	wenzelm
	Fri, 07 Dec 2012 18:05:24 +0100
changeset 51441	d2c60ada3ece
parent 50000	5386df44a037
child 53879	e7296939fec2
permissions	-rw-r--r--