doc-src/Codegen/codegen.tex

stub for evaluation chapter

+
−
+
−\documentclass[12pt,a4paper,fleqn]{article}
+
−\usepackage{latexsym,graphicx}
+
−\usepackage[refpage]{nomencl}
+
−\usepackage{../iman,../extra,../isar,../proof}
+
−\usepackage{../isabelle,../isabellesym}
+
−\usepackage{style}
+
−\usepackage{../pdfsetup}
+
−
+
−\hyphenation{Isabelle}
+
−\hyphenation{Isar}
+
−\isadroptag{theory}
+
−
+
−\title{\includegraphics[scale=0.5]{isabelle_isar}
+
−  \\[4ex] Code generation from Isabelle/HOL theories}
+
−\author{\emph{Florian Haftmann with contributions from Lukas Bulwahn}}
+
−
+
−\begin{document}
+
−
+
−\maketitle
+
−
+
−\begin{abstract}
+
−  \noindent This tutorial introduces the code generator facilities of Isabelle/HOL.
+
−    They empower the user to turn HOL specifications into corresponding executable
+
−    programs in the languages SML, OCaml and Haskell.
+
−\end{abstract}
+
−
+
−\thispagestyle{empty}\clearpage
+
−
+
−\pagenumbering{roman}
+
−\clearfirst
+
−
+
−\input{Thy/document/Introduction.tex}
+
−\input{Thy/document/Foundations.tex}
+
−\input{Thy/document/Refinement.tex}
+
−\input{Thy/document/Inductive_Predicate.tex}
+
−\input{Thy/document/Adaptation.tex}
+
−\input{Thy/document/Evaluation.tex}
+
−\input{Thy/document/Further.tex}
+
−
+
−\begingroup
+
−\bibliographystyle{plain} \small\raggedright\frenchspacing
+
−\bibliography{../manual}
+
−\endgroup
+
−
+
−\end{document}
+
−
+
−
+
−%%% Local Variables: 
+
−%%% mode: latex
+
−%%% TeX-master: t
+
−%%% End: