src/HOL/MicroJava/document/root.tex
author haftmann
Tue Nov 24 14:37:23 2009 +0100 (2009-11-24)
changeset 33954 1bc3b688548c
parent 17159 d5060118122e
child 55369 713629c2b73c
permissions -rwxr-xr-x
backported parts of abstract byte code verifier from AFP/Jinja
     1 % $Id$
     2 
     3 %\documentclass[11pt,a4paper]{article}
     4 \documentclass[11pt,a4paper]{book}
     5 \usepackage{graphicx,latexsym,isabelle,isabellesym,pdfsetup}
     6 
     7 \urlstyle{rm}
     8 \pagestyle{myheadings}
     9 
    10 %make a bit more space
    11 \addtolength{\hoffset}{-1,5cm}
    12 \addtolength{\textwidth}{3cm}
    13 \addtolength{\voffset}{-1cm}
    14 \addtolength{\textheight}{2cm}
    15 
    16 \newcommand{\isaheader}[1]
    17 {\newpage\markright{Theory~\isabellecontext}\section{#1}}
    18 \renewcommand{\isamarkupheader}[1]{#1}
    19 \renewcommand{\isamarkupsection}[1]{\subsection{#1}}
    20 
    21 \newcommand{\mJava}{$\mu$Java}
    22 \newcommand{\secref}[1]{Section~\ref{#1}}
    23 \newcommand{\secrefs}[1]{Sections~\ref{#1}}
    24 \newcommand{\charef}[1]{Chapter~\ref{#1}}
    25 \newcommand{\charefs}[1]{Chapters~\ref{#1}}
    26 
    27 %remove clutter from the toc
    28 \setcounter{secnumdepth}{2}
    29 \setcounter{tocdepth}{1}
    30 
    31 \begin{document}
    32 
    33 \title{Java Source and Bytecode Formalizations in Isabelle: \mJava}
    34 \author{Gerwin Klein \and Tobias Nipkow \and David von Oheimb \and
    35   \and Cornelia Pusch \and Martin Strecker}
    36 \maketitle
    37 
    38 
    39 \tableofcontents
    40 \parindent 0pt \parskip 0.5ex
    41 
    42 \input{introduction.tex}
    43 
    44 \section{Theory Dependencies}
    45 
    46 Figure \ref{theory-deps} shows the dependencies between 
    47 the Isabelle theories in the following sections.
    48 
    49 \begin{figure}[h!t]
    50 \begin{center}
    51   \includegraphics[width=\textwidth,height=0.95\textheight,keepaspectratio]{session_graph}
    52 \end{center}
    53 \caption{Theory Dependency Graph\label{theory-deps}}
    54 \end{figure}
    55 
    56 \newpage
    57 \input{session}
    58 
    59 \newpage
    60 \nocite{*}
    61 \bibliographystyle{abbrv}
    62 \bibliography{root}
    63 
    64 \end{document}