author | kleing |
Thu, 21 Feb 2002 13:37:09 +0100 | |
changeset 12914 | 71015f46b3c1 |
parent 12911 | 704713ca07ea |
child 17159 | d5060118122e |
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} |
12914 | 10 |
\addtolength{\textwidth}{3cm} |
11 |
\addtolength{\voffset}{-1cm} |
|
12 |
\addtolength{\textheight}{2cm} |
|
9755 | 13 |
|
12911 | 14 |
\newcommand{\isaheader}[1] |
12914 | 15 |
{\newpage\markright{Theory~\isabellecontext}\section{#1}} |
12911 | 16 |
\renewcommand{\isamarkupheader}[1]{#1} |
12914 | 17 |
\renewcommand{\isamarkupsection}[1]{\subsection{#1}} |
10044
07218d743c62
tuned, added lightweight BV to abstract, added Bali link
kleing
parents:
10023
diff
changeset
|
18 |
|
9985 | 19 |
\newcommand{\mJava}{$\mu$Java} |
12911 | 20 |
\newcommand{\secref}[1]{Section~\ref{#1}} |
21 |
\newcommand{\secrefs}[1]{Sections~\ref{#1}} |
|
22 |
\newcommand{\charef}[1]{Chapter~\ref{#1}} |
|
23 |
\newcommand{\charefs}[1]{Chapters~\ref{#1}} |
|
24 |
||
10044
07218d743c62
tuned, added lightweight BV to abstract, added Bali link
kleing
parents:
10023
diff
changeset
|
25 |
%remove clutter from the toc |
12914 | 26 |
\setcounter{secnumdepth}{2} |
27 |
\setcounter{tocdepth}{1} |
|
10044
07218d743c62
tuned, added lightweight BV to abstract, added Bali link
kleing
parents:
10023
diff
changeset
|
28 |
|
8193 | 29 |
\begin{document} |
9820 | 30 |
|
12911 | 31 |
\title{Java Source and Bytecode Formalizations in Isabelle: \mJava\\ |
32 |
% {\large -- VerifiCard Project Deliverables -- } |
|
33 |
} |
|
34 |
\author{Gerwin Klein \and Tobias Nipkow \and David von Oheimb \and |
|
12914 | 35 |
\and Cornelia Pusch \and Martin Strecker} |
9919 | 36 |
\maketitle |
37 |
||
38 |
||
9755 | 39 |
\tableofcontents |
9820 | 40 |
\parindent 0pt \parskip 0.5ex |
9919 | 41 |
|
12911 | 42 |
\input{introduction.tex} |
43 |
||
12914 | 44 |
\section{Theory Dependencies} |
12911 | 45 |
|
46 |
Figure \ref{theory-deps} shows the dependencies between |
|
47 |
the Isabelle theories in the following sections. |
|
48 |
||
12914 | 49 |
\begin{figure}[h!t] |
11855 | 50 |
\begin{center} |
51 |
\includegraphics[scale=0.4]{session_graph} |
|
52 |
\end{center} |
|
12911 | 53 |
\caption{Theory Dependency Graph\label{theory-deps}} |
54 |
\end{figure} |
|
11855 | 55 |
|
9755 | 56 |
\newpage |
8193 | 57 |
\input{session} |
9820 | 58 |
|
10044
07218d743c62
tuned, added lightweight BV to abstract, added Bali link
kleing
parents:
10023
diff
changeset
|
59 |
\newpage |
9919 | 60 |
\nocite{*} |
61 |
\bibliographystyle{abbrv} |
|
62 |
\bibliography{root} |
|
63 |
||
8193 | 64 |
\end{document} |