5 \urlstyle{rm} |
5 \urlstyle{rm} |
6 \pagestyle{myheadings} |
6 \pagestyle{myheadings} |
7 |
7 |
8 %make a bit more space |
8 %make a bit more space |
9 \addtolength{\hoffset}{-1,5cm} |
9 \addtolength{\hoffset}{-1,5cm} |
10 \addtolength{\textwidth}{4cm} |
10 \addtolength{\textwidth}{3cm} |
11 \addtolength{\voffset}{-2cm} |
11 \addtolength{\voffset}{-1cm} |
12 \addtolength{\textheight}{4cm} |
12 \addtolength{\textheight}{2cm} |
13 |
13 |
14 %subsection instead of section to make the toc readable |
|
15 \newcommand{\isaheader}[1] |
14 \newcommand{\isaheader}[1] |
16 {\newpage\markright{Theory~\isabellecontext}\subsection{#1}} |
15 {\newpage\markright{Theory~\isabellecontext}\section{#1}} |
17 \renewcommand{\thesubsection}{\arabic{subsection}} |
|
18 \renewcommand{\isamarkupheader}[1]{#1} |
16 \renewcommand{\isamarkupheader}[1]{#1} |
19 \renewcommand{\isamarkupsection}[1]{\subsubsection{#1}} |
17 \renewcommand{\isamarkupsection}[1]{\subsection{#1}} |
20 \renewcommand{\isamarkupsubsection}[1]{\subsubsection{#1}} |
|
21 |
|
22 %remove spaces from the isabelle environment (trivlist makes them too large) |
|
23 %\renewenvironment{isabelle} |
|
24 %{\begin{isabellebody}} |
|
25 %{\end{isabellebody}} |
|
26 |
|
27 |
18 |
28 \newcommand{\mJava}{$\mu$Java} |
19 \newcommand{\mJava}{$\mu$Java} |
29 \newcommand{\secref}[1]{Section~\ref{#1}} |
20 \newcommand{\secref}[1]{Section~\ref{#1}} |
30 \newcommand{\secrefs}[1]{Sections~\ref{#1}} |
21 \newcommand{\secrefs}[1]{Sections~\ref{#1}} |
31 \newcommand{\charef}[1]{Chapter~\ref{#1}} |
22 \newcommand{\charef}[1]{Chapter~\ref{#1}} |
32 \newcommand{\charefs}[1]{Chapters~\ref{#1}} |
23 \newcommand{\charefs}[1]{Chapters~\ref{#1}} |
33 |
24 |
34 |
|
35 %remove clutter from the toc |
25 %remove clutter from the toc |
36 \setcounter{secnumdepth}{3} |
26 \setcounter{secnumdepth}{2} |
37 \setcounter{tocdepth}{2} |
27 \setcounter{tocdepth}{1} |
38 |
28 |
39 \begin{document} |
29 \begin{document} |
40 |
30 |
41 \title{Java Source and Bytecode Formalizations in Isabelle: \mJava\\ |
31 \title{Java Source and Bytecode Formalizations in Isabelle: \mJava\\ |
42 % {\large -- VerifiCard Project Deliverables -- } |
32 % {\large -- VerifiCard Project Deliverables -- } |
43 } |
33 } |
44 \author{Gerwin Klein \and Tobias Nipkow \and David von Oheimb \and |
34 \author{Gerwin Klein \and Tobias Nipkow \and David von Oheimb \and |
45 Leonor Prensa Nieto \and Norbert Schirmer \and Martin Strecker} |
35 \and Cornelia Pusch \and Martin Strecker} |
46 \maketitle |
36 \maketitle |
47 |
37 |
48 |
38 |
49 \tableofcontents |
39 \tableofcontents |
50 \parindent 0pt \parskip 0.5ex |
40 \parindent 0pt \parskip 0.5ex |
51 |
41 |
52 \input{introduction.tex} |
42 \input{introduction.tex} |
53 |
43 |
54 \section*{Theory Dependencies} |
44 \section{Theory Dependencies} |
55 |
45 |
56 Figure \ref{theory-deps} shows the dependencies between |
46 Figure \ref{theory-deps} shows the dependencies between |
57 the Isabelle theories in the following sections. |
47 the Isabelle theories in the following sections. |
58 |
48 |
59 \begin{figure} |
49 \begin{figure}[h!t] |
60 \begin{center} |
50 \begin{center} |
61 \includegraphics[scale=0.4]{session_graph} |
51 \includegraphics[scale=0.4]{session_graph} |
62 \end{center} |
52 \end{center} |
63 \caption{Theory Dependency Graph\label{theory-deps}} |
53 \caption{Theory Dependency Graph\label{theory-deps}} |
64 \end{figure} |
54 \end{figure} |