src/HOL/MicroJava/document/root.tex
changeset 9764 fa4f45fa4666
parent 9755 6fefedeb3428
child 9820 2aa2871d0dec
equal deleted inserted replaced
9763:252c690690b0 9764:fa4f45fa4666
     8 \addtolength{\hoffset}{-1,5cm}
     8 \addtolength{\hoffset}{-1,5cm}
     9 \addtolength{\textwidth}{4cm}
     9 \addtolength{\textwidth}{4cm}
    10 \addtolength{\voffset}{-2cm}
    10 \addtolength{\voffset}{-2cm}
    11 \addtolength{\textheight}{4cm}
    11 \addtolength{\textheight}{4cm}
    12 
    12 
       
    13 \renewcommand{\thesubsection}{\arabic{subsection}}
       
    14 \renewcommand{\isamarkupheader}[1]{\newpage\subsection{#1}}
       
    15 
    13 \pagestyle{headings}
    16 \pagestyle{headings}
    14 
    17 
    15 \begin{document}
    18 \begin{document}
    16 
       
    17 \tableofcontents
    19 \tableofcontents
    18 \newpage
    20 \newpage
    19 \input{session}
    21 \input{session}
    20 \end{document}
    22 \end{document}
    21