tuned, added lightweight BV to abstract, added Bali link
authorkleing
Thu Sep 21 12:13:36 2000 +0200 (2000-09-21)
changeset 1004407218d743c62
parent 10043 a0364652e115
child 10045 c76b73e16711
tuned, added lightweight BV to abstract, added Bali link
src/HOL/MicroJava/document/root.tex
     1.1 --- a/src/HOL/MicroJava/document/root.tex	Thu Sep 21 12:11:38 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/document/root.tex	Thu Sep 21 12:13:36 2000 +0200
     1.3 @@ -10,22 +10,36 @@
     1.4  \addtolength{\voffset}{-2cm}
     1.5  \addtolength{\textheight}{4cm}
     1.6  
     1.7 -\renewcommand{\thesection}{\arabic{section}}
     1.8 -\renewcommand{\isamarkupheader}[1]{\newpage\markright{Theory~\isabellecontext}\section{#1}}
     1.9 +%subsection instead of section to make the toc readable
    1.10 +\renewcommand{\thesubsection}{\arabic{subsection}}
    1.11 +\renewcommand{\isamarkupheader}[1]{\newpage\markright{Theory~\isabellecontext}\subsection{#1}}
    1.12 +
    1.13 +%remove spaces from the isabelle environment (trivlist makes them too large)
    1.14 +\renewenvironment{isabelle}
    1.15 +{\begin{isabellebody}}
    1.16 +{\end{isabellebody}}
    1.17 +
    1.18  \newcommand{\mJava}{$\mu$Java}
    1.19  
    1.20 +%remove clutter from the toc
    1.21 +\setcounter{secnumdepth}{2}
    1.22 +\setcounter{tocdepth}{2}
    1.23 +
    1.24  \begin{document}
    1.25  
    1.26  \title{\mJava}
    1.27  \author{Gerwin Klein \\ Tobias Nipkow \\ David von Oheimb \\ Cornelia Pusch}
    1.28  \maketitle
    1.29  
    1.30 -\begin{abstract}
    1.31 +\begin{abstract}\noindent
    1.32    This formal development defines {\mJava}, a small fragment of the
    1.33    programming language Java (with essentially just classes), together with a
    1.34 -  corresponding virtual machine and a specification of its bytecode verifier.
    1.35 +  corresponding virtual machine, a specification of its bytecode verifier
    1.36 +  and a lightweight bytecode verifier.
    1.37    It is shown that {\mJava} and the given specification of the bytecode
    1.38 -  verifier are type-safe.
    1.39 +  verifier are type-safe, and that the lightweight bytecode verifier
    1.40 +  is functionally equivalent to the bytecode verifier specification.
    1.41 +  See also the homepage of project Bali at \url{http://isabelle.in.tum.de/Bali/}.
    1.42  \end{abstract}
    1.43  
    1.44  \tableofcontents
    1.45 @@ -34,6 +48,7 @@
    1.46  \newpage
    1.47  \input{session}
    1.48  
    1.49 +\newpage
    1.50  \nocite{*}
    1.51  \bibliographystyle{abbrv}
    1.52  \bibliography{root}