# HG changeset patch
# User wenzelm
# Date 968686841 -7200
# Node ID 3cf12ab0b8aca356e950532eac2a21e75dcdb29f
# Parent  dab013ea6b6382803b92deffbc78cb6700ea14b8
added title, abstract, bibliography;

diff -r dab013ea6b63 -r 3cf12ab0b8ac src/HOL/MicroJava/document/root.tex
--- a/src/HOL/MicroJava/document/root.tex	Mon Sep 11 17:39:18 2000 +0200
+++ b/src/HOL/MicroJava/document/root.tex	Mon Sep 11 17:40:41 2000 +0200
@@ -2,23 +2,39 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{isabelle,isabellesym,pdfsetup}
 
+\pagestyle{myheadings}
+
 \addtolength{\hoffset}{-1,5cm}
 \addtolength{\textwidth}{4cm}
 \addtolength{\voffset}{-2cm}
 \addtolength{\textheight}{4cm}
 
 \renewcommand{\thesection}{\arabic{section}}
-\renewcommand{\isamarkupheader}[1]{\newpage\section{#1}}
-
-\pagestyle{headings}
+\renewcommand{\isamarkupheader}[1]{\newpage\markright{Theory~\isabellecontext}\section{#1}}
 
 
 \begin{document}
 
+\title{$\mu$Java}
+\author{Gerwin Klein \\ Tobias Nipkow \\ David von Oheimb \\ Cornelia Pusch}
+\maketitle
+
+\begin{abstract}
+  This formal development defines Micro Java, a small fragment of the
+  programming language Java (essentially just classes), together with a
+  corresponding virtual machine and a specification of its bytecode verifier.
+  It is shown that Micro Java and the given specification of the bytecode
+  verifier are type safe.
+\end{abstract}
+
 \tableofcontents
 \parindent 0pt \parskip 0.5ex
+
 \newpage
-
 \input{session}
 
+\nocite{*}
+\bibliographystyle{abbrv}
+\bibliography{root}
+
 \end{document}