tuned
authorkleing
Thu, 31 Aug 2000 14:11:04 +0200
changeset 9764 fa4f45fa4666
parent 9763 252c690690b0
child 9765 46def28153d6
tuned
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}
-