# HG changeset patch
# User kleing
# Date 967723864 -7200
# Node ID fa4f45fa4666583e82c0e7767c125dd9a3418214
# Parent  252c690690b00ac48081ac12cc7caa38060ca531
tuned

diff -r 252c690690b0 -r fa4f45fa4666 src/HOL/MicroJava/document/root.tex
--- a/src/HOL/MicroJava/document/root.tex	Thu Aug 31 09:23:01 2000 +0200
+++ b/src/HOL/MicroJava/document/root.tex	Thu Aug 31 14:11:04 2000 +0200
@@ -10,12 +10,13 @@
 \addtolength{\voffset}{-2cm}
 \addtolength{\textheight}{4cm}
 
+\renewcommand{\thesubsection}{\arabic{subsection}}
+\renewcommand{\isamarkupheader}[1]{\newpage\subsection{#1}}
+
 \pagestyle{headings}
 
 \begin{document}
-
 \tableofcontents
 \newpage
 \input{session}
 \end{document}
-