%\documentclass[11pt,a4paper]{article}
\documentclass[11pt,a4paper]{book}
\usepackage{graphicx,latexsym,isabelle,isabellesym,pdfsetup}
\urlstyle{rm}
\pagestyle{myheadings}
%make a bit more space
\addtolength{\hoffset}{-1,5cm}
\addtolength{\textwidth}{4cm}
\addtolength{\voffset}{-2cm}
\addtolength{\textheight}{4cm}
%subsection instead of section to make the toc readable
\newcommand{\isaheader}[1]
{\newpage\markright{Theory~\isabellecontext}\subsection{#1}}
\renewcommand{\thesubsection}{\arabic{subsection}}
\renewcommand{\isamarkupheader}[1]{#1}
\renewcommand{\isamarkupsection}[1]{\subsubsection{#1}}
\renewcommand{\isamarkupsubsection}[1]{\subsubsection{#1}}
%remove spaces from the isabelle environment (trivlist makes them too large)
%\renewenvironment{isabelle}
%{\begin{isabellebody}}
%{\end{isabellebody}}
\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}{3}
\setcounter{tocdepth}{2}
\begin{document}
\title{Java Source and Bytecode Formalizations in Isabelle: \mJava\\
% {\large -- VerifiCard Project Deliverables -- }
}
\author{Gerwin Klein \and Tobias Nipkow \and David von Oheimb \and
Leonor Prensa Nieto \and Norbert Schirmer \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}
\begin{center}
\includegraphics[scale=0.4]{session_graph}
\end{center}
\caption{Theory Dependency Graph\label{theory-deps}}
\end{figure}
\newpage
\input{session}
\newpage
\nocite{*}
\bibliographystyle{abbrv}
\bibliography{root}
\end{document}