1\documentclass[11pt,a4paper]{book} 2\usepackage{graphicx,latexsym,isabelle,isabellesym,pdfsetup} 3 4\urlstyle{rm} 5\pagestyle{myheadings} 6 7%make a bit more space 8\addtolength{\hoffset}{-1,5cm} 9\addtolength{\textwidth}{3cm} 10\addtolength{\voffset}{-1cm} 11\addtolength{\textheight}{2cm} 12 13\renewcommand{\setisabellecontext}[1]{\markright{Theory~#1}} 14 15\newcommand{\mJava}{$\mu$Java} 16\newcommand{\secref}[1]{Section~\ref{#1}} 17\newcommand{\secrefs}[1]{Sections~\ref{#1}} 18\newcommand{\charef}[1]{Chapter~\ref{#1}} 19\newcommand{\charefs}[1]{Chapters~\ref{#1}} 20 21%remove clutter from the toc 22\setcounter{secnumdepth}{2} 23\setcounter{tocdepth}{1} 24 25\begin{document} 26 27\title{Java Source and Bytecode Formalizations in Isabelle: \mJava} 28\author{Gerwin Klein \and Tobias Nipkow \and David von Oheimb \and 29 \and Cornelia Pusch \and Martin Strecker} 30\maketitle 31 32 33\tableofcontents 34\parindent 0pt \parskip 0.5ex 35 36\input{introduction.tex} 37 38\section{Theory Dependencies} 39 40Figure \ref{theory-deps} shows the dependencies between 41the Isabelle theories in the following sections. 42 43\begin{figure}[h!t] 44\begin{center} 45 \includegraphics[width=\textwidth,height=0.95\textheight,keepaspectratio]{session_graph} 46\end{center} 47\caption{Theory Dependency Graph\label{theory-deps}} 48\end{figure} 49 50\newpage 51\input{session} 52 53\newpage 54\nocite{*} 55\bibliographystyle{abbrv} 56\bibliography{root} 57 58\end{document} 59