doc-src/IsarAdvanced/Codegen/codegen.tex

re-canibalised manual

%% $Id$

\documentclass[12pt,a4paper,fleqn]{report}
\usepackage{latexsym,graphicx}
\usepackage{listings}
\usepackage[refpage]{nomencl}
\usepackage{../../iman,../../extra,../../isar,../../proof}
\usepackage{../../isabelle,../../isabellesym}
\usepackage{style}
\usepackage{../../pdfsetup}

\makeatletter

\newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
\isakeeptag{quoteme}
\newenvironment{quoteme}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
\renewcommand{\isatagquoteme}{\begin{quoteme}}
\renewcommand{\endisatagquoteme}{\end{quoteme}}

\makeatother

\isakeeptag{tt}
\renewcommand{\isatagtt}{\isabellestyle{tt}\isastyle}
\renewcommand{\endisatagtt}{\isabellestyle{it}\isastyle}

\newcommand{\qt}[1]{``#1''}
\newcommand{\qtt}[1]{"{}{#1}"{}}
\newcommand{\qn}[1]{\emph{#1}}
\newcommand{\strong}[1]{{\bfseries #1}}
\newcommand{\fixme}[1][!]{\strong{FIXME: #1}}

\hyphenation{Isabelle}
\hyphenation{Isar}

\isadroptag{theory}
\title{\includegraphics[scale=0.5]{isabelle_isar}
  \\[4ex] Code generation from Isabelle/HOL theories}
\author{\emph{Florian Haftmann}}


\begin{document}

\maketitle

\begin{abstract}
  This tutorial gives am introduction to a generic code generator framework in Isabelle
  for generating executable code in functional programming languages from logical
  specifications in Isabelle/HOL.
\end{abstract}

\thispagestyle{empty}\clearpage

\pagenumbering{roman}
\clearfirst

\input{Thy/document/Introduction.tex}
\input{Thy/document/Program.tex}
\input{Thy/document/Adaption.tex}
\input{Thy/document/Further.tex}
\input{Thy/document/ML.tex}

\begingroup
%\tocentry{\bibname}
\bibliographystyle{plain} \small\raggedright\frenchspacing
\bibliography{../../manual}
\endgroup

\end{document}


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: