--- a/src/HOL/MicroJava/document/introduction.tex Thu Feb 21 11:05:20 2002 +0100
+++ b/src/HOL/MicroJava/document/introduction.tex Thu Feb 21 13:37:09 2002 +0100
@@ -1,5 +1,6 @@
+\chapter{Preface}
-\section*{Introduction}
+\section{Introduction}
\label{sec:introduction}
This document contains the automatically generated listings of the
--- a/src/HOL/MicroJava/document/root.tex Thu Feb 21 11:05:20 2002 +0100
+++ b/src/HOL/MicroJava/document/root.tex Thu Feb 21 13:37:09 2002 +0100
@@ -7,23 +7,14 @@
%make a bit more space
\addtolength{\hoffset}{-1,5cm}
-\addtolength{\textwidth}{4cm}
-\addtolength{\voffset}{-2cm}
-\addtolength{\textheight}{4cm}
+\addtolength{\textwidth}{3cm}
+\addtolength{\voffset}{-1cm}
+\addtolength{\textheight}{2cm}
-%subsection instead of section to make the toc readable
\newcommand{\isaheader}[1]
-{\newpage\markright{Theory~\isabellecontext}\subsection{#1}}
-\renewcommand{\thesubsection}{\arabic{subsection}}
+{\newpage\markright{Theory~\isabellecontext}\section{#1}}
\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}}
-
+\renewcommand{\isamarkupsection}[1]{\subsection{#1}}
\newcommand{\mJava}{$\mu$Java}
\newcommand{\secref}[1]{Section~\ref{#1}}
@@ -31,10 +22,9 @@
\newcommand{\charef}[1]{Chapter~\ref{#1}}
\newcommand{\charefs}[1]{Chapters~\ref{#1}}
-
%remove clutter from the toc
-\setcounter{secnumdepth}{3}
-\setcounter{tocdepth}{2}
+\setcounter{secnumdepth}{2}
+\setcounter{tocdepth}{1}
\begin{document}
@@ -42,7 +32,7 @@
% {\large -- VerifiCard Project Deliverables -- }
}
\author{Gerwin Klein \and Tobias Nipkow \and David von Oheimb \and
- Leonor Prensa Nieto \and Norbert Schirmer \and Martin Strecker}
+ \and Cornelia Pusch \and Martin Strecker}
\maketitle
@@ -51,12 +41,12 @@
\input{introduction.tex}
-\section*{Theory Dependencies}
+\section{Theory Dependencies}
Figure \ref{theory-deps} shows the dependencies between
the Isabelle theories in the following sections.
-\begin{figure}
+\begin{figure}[h!t]
\begin{center}
\includegraphics[scale=0.4]{session_graph}
\end{center}