src/HOL/NanoJava/document/root.tex
author wenzelm
Sun Sep 18 20:33:48 2016 +0200 (2016-09-18)
changeset 63915 bab633745c7f
parent 11855 bdae1f29f35d
child 68649 f849fc1cb65e
permissions -rw-r--r--
tuned proofs;
     1 \documentclass[11pt,a4paper]{article}
     2 \usepackage{graphicx,latexsym,isabelle,isabellesym,latexsym,pdfsetup}
     3 
     4 \urlstyle{tt}
     5 \pagestyle{myheadings}
     6 
     7 \addtolength{\hoffset}{-1,5cm}
     8 \addtolength{\textwidth}{4cm}
     9 \addtolength{\voffset}{-2cm}
    10 \addtolength{\textheight}{4cm}
    11 
    12 %remove spaces from the isabelle environment (trivlist makes them too large)
    13 \renewenvironment{isabelle}
    14 {\begin{isabellebody}}
    15 {\end{isabellebody}}
    16 
    17 \newcommand{\nJava}{\it NanoJava}
    18 
    19 %remove clutter from the toc
    20 \setcounter{secnumdepth}{3}
    21 \setcounter{tocdepth}{2}
    22 
    23 \begin{document}
    24 
    25 \title{\nJava}
    26 \author{David von Oheimb \\ Tobias Nipkow}
    27 \maketitle
    28 
    29 \begin{abstract}\noindent
    30   These theories define {\nJava}, a very small fragment of the programming 
    31   language Java (with essentially just classes) derived from the one given 
    32   in \cite{NipkowOP00}.
    33   For {\nJava}, an operational semantics is given as well as a Hoare logic,
    34   which is proved both sound and (relatively) complete. 
    35   The Hoare logic supports side-effecting expressions and
    36   implements a new approach for handling auxiliary variables.
    37   A more complex Hoare logic covering a much larger subset of Java is described
    38   in \cite{DvO-CPE01}.\\
    39 See also the homepage of project Bali at \url{http://isabelle.in.tum.de/Bali/}
    40 and the conference version of this document \cite{NanoJava}.
    41 \end{abstract}
    42 
    43 \tableofcontents
    44 \parindent 0pt \parskip 0.5ex
    45 
    46 \begin{center}
    47   \includegraphics[scale=0.7]{session_graph}  
    48 \end{center}
    49 
    50 \newpage
    51 \input{session}
    52 
    53 \newpage
    54 \nocite{*}
    55 \bibliographystyle{abbrv}
    56 \bibliography{root}
    57 
    58 \end{document}