src/HOL/MicroJava/document/root.tex
 author wenzelm Sun, 09 Feb 2014 17:41:17 +0100 changeset 55369 713629c2b73c parent 17159 d5060118122e child 58886 8a6cac7c7247 permissions -rw-r--r--
removed junk;

\documentclass[11pt,a4paper]{book}
\usepackage{graphicx,latexsym,isabelle,isabellesym,pdfsetup}

\urlstyle{rm}

%make a bit more space

{\newpage\markright{Theory~\isabellecontext}\section{#1}}
\renewcommand{\isamarkupsection}[1]{\subsection{#1}}

\newcommand{\mJava}{$\mu$Java}
\newcommand{\secref}[1]{Section~\ref{#1}}
\newcommand{\secrefs}[1]{Sections~\ref{#1}}
\newcommand{\charef}[1]{Chapter~\ref{#1}}
\newcommand{\charefs}[1]{Chapters~\ref{#1}}

%remove clutter from the toc
\setcounter{secnumdepth}{2}
\setcounter{tocdepth}{1}

\begin{document}

\title{Java Source and Bytecode Formalizations in Isabelle: \mJava}
\author{Gerwin Klein \and Tobias Nipkow \and David von Oheimb \and
\and Cornelia Pusch \and Martin Strecker}
\maketitle

\tableofcontents
\parindent 0pt \parskip 0.5ex

\input{introduction.tex}

\section{Theory Dependencies}

Figure \ref{theory-deps} shows the dependencies between
the Isabelle theories in the following sections.

\begin{figure}[h!t]
\begin{center}
\includegraphics[width=\textwidth,height=0.95\textheight,keepaspectratio]{session_graph}
\end{center}
\caption{Theory Dependency Graph\label{theory-deps}}
\end{figure}

\newpage
\input{session}

\newpage
\nocite{*}
\bibliographystyle{abbrv}
\bibliography{root}

\end{document}