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}
-