author | kleing |
Thu, 21 Feb 2002 09:54:08 +0100 | |
changeset 12911 | 704713ca07ea |
parent 11855 | bdae1f29f35d |
child 12914 | 71015f46b3c1 |
permissions | -rw-r--r-- |
12911 | 1 |
%\documentclass[11pt,a4paper]{article} |
2 |
\documentclass[11pt,a4paper]{book} |
|
11855 | 3 |
\usepackage{graphicx,latexsym,isabelle,isabellesym,pdfsetup} |
8193 | 4 |
|
10023 | 5 |
\urlstyle{rm} |
9919 | 6 |
\pagestyle{myheadings} |
7 |
||
12911 | 8 |
%make a bit more space |
9755 | 9 |
\addtolength{\hoffset}{-1,5cm} |
10 |
\addtolength{\textwidth}{4cm} |
|
11 |
\addtolength{\voffset}{-2cm} |
|
12 |
\addtolength{\textheight}{4cm} |
|
13 |
||
10044
07218d743c62
tuned, added lightweight BV to abstract, added Bali link
kleing
parents:
10023
diff
changeset
|
14 |
%subsection instead of section to make the toc readable |
12911 | 15 |
\newcommand{\isaheader}[1] |
16 |
{\newpage\markright{Theory~\isabellecontext}\subsection{#1}} |
|
10044
07218d743c62
tuned, added lightweight BV to abstract, added Bali link
kleing
parents:
10023
diff
changeset
|
17 |
\renewcommand{\thesubsection}{\arabic{subsection}} |
12911 | 18 |
\renewcommand{\isamarkupheader}[1]{#1} |
11075 | 19 |
\renewcommand{\isamarkupsection}[1]{\subsubsection{#1}} |
12911 | 20 |
\renewcommand{\isamarkupsubsection}[1]{\subsubsection{#1}} |
10044
07218d743c62
tuned, added lightweight BV to abstract, added Bali link
kleing
parents:
10023
diff
changeset
|
21 |
|
07218d743c62
tuned, added lightweight BV to abstract, added Bali link
kleing
parents:
10023
diff
changeset
|
22 |
%remove spaces from the isabelle environment (trivlist makes them too large) |
12911 | 23 |
%\renewenvironment{isabelle} |
24 |
%{\begin{isabellebody}} |
|
25 |
%{\end{isabellebody}} |
|
26 |
||
10044
07218d743c62
tuned, added lightweight BV to abstract, added Bali link
kleing
parents:
10023
diff
changeset
|
27 |
|
9985 | 28 |
\newcommand{\mJava}{$\mu$Java} |
12911 | 29 |
\newcommand{\secref}[1]{Section~\ref{#1}} |
30 |
\newcommand{\secrefs}[1]{Sections~\ref{#1}} |
|
31 |
\newcommand{\charef}[1]{Chapter~\ref{#1}} |
|
32 |
\newcommand{\charefs}[1]{Chapters~\ref{#1}} |
|
33 |
||
9820 | 34 |
|
10044
07218d743c62
tuned, added lightweight BV to abstract, added Bali link
kleing
parents:
10023
diff
changeset
|
35 |
%remove clutter from the toc |
11075 | 36 |
\setcounter{secnumdepth}{3} |
10044
07218d743c62
tuned, added lightweight BV to abstract, added Bali link
kleing
parents:
10023
diff
changeset
|
37 |
\setcounter{tocdepth}{2} |
07218d743c62
tuned, added lightweight BV to abstract, added Bali link
kleing
parents:
10023
diff
changeset
|
38 |
|
8193 | 39 |
\begin{document} |
9820 | 40 |
|
12911 | 41 |
\title{Java Source and Bytecode Formalizations in Isabelle: \mJava\\ |
42 |
% {\large -- VerifiCard Project Deliverables -- } |
|
43 |
} |
|
44 |
\author{Gerwin Klein \and Tobias Nipkow \and David von Oheimb \and |
|
45 |
Leonor Prensa Nieto \and Norbert Schirmer \and Martin Strecker} |
|
9919 | 46 |
\maketitle |
47 |
||
48 |
||
9755 | 49 |
\tableofcontents |
9820 | 50 |
\parindent 0pt \parskip 0.5ex |
9919 | 51 |
|
12911 | 52 |
\input{introduction.tex} |
53 |
||
54 |
\section*{Theory Dependencies} |
|
55 |
||
56 |
Figure \ref{theory-deps} shows the dependencies between |
|
57 |
the Isabelle theories in the following sections. |
|
58 |
||
59 |
\begin{figure} |
|
11855 | 60 |
\begin{center} |
61 |
\includegraphics[scale=0.4]{session_graph} |
|
62 |
\end{center} |
|
12911 | 63 |
\caption{Theory Dependency Graph\label{theory-deps}} |
64 |
\end{figure} |
|
11855 | 65 |
|
9755 | 66 |
\newpage |
8193 | 67 |
\input{session} |
9820 | 68 |
|
10044
07218d743c62
tuned, added lightweight BV to abstract, added Bali link
kleing
parents:
10023
diff
changeset
|
69 |
\newpage |
9919 | 70 |
\nocite{*} |
71 |
\bibliographystyle{abbrv} |
|
72 |
\bibliography{root} |
|
73 |
||
8193 | 74 |
\end{document} |