src/HOL/MicroJava/document/root.tex
changeset 58886 8a6cac7c7247
parent 55369 713629c2b73c
child 73404 299f6a8faccc
equal deleted inserted replaced
58885:47fdd4f40d00 58886:8a6cac7c7247
     8 \addtolength{\hoffset}{-1,5cm}
     8 \addtolength{\hoffset}{-1,5cm}
     9 \addtolength{\textwidth}{3cm}
     9 \addtolength{\textwidth}{3cm}
    10 \addtolength{\voffset}{-1cm}
    10 \addtolength{\voffset}{-1cm}
    11 \addtolength{\textheight}{2cm}
    11 \addtolength{\textheight}{2cm}
    12 
    12 
    13 \newcommand{\isaheader}[1]
    13 \renewcommand{\setisabellecontext}[1]{\markright{Theory~#1}}
    14 {\newpage\markright{Theory~\isabellecontext}\section{#1}}
       
    15 \renewcommand{\isamarkupheader}[1]{#1}
       
    16 \renewcommand{\isamarkupsection}[1]{\subsection{#1}}
       
    17 
    14 
    18 \newcommand{\mJava}{$\mu$Java}
    15 \newcommand{\mJava}{$\mu$Java}
    19 \newcommand{\secref}[1]{Section~\ref{#1}}
    16 \newcommand{\secref}[1]{Section~\ref{#1}}
    20 \newcommand{\secrefs}[1]{Sections~\ref{#1}}
    17 \newcommand{\secrefs}[1]{Sections~\ref{#1}}
    21 \newcommand{\charef}[1]{Chapter~\ref{#1}}
    18 \newcommand{\charef}[1]{Chapter~\ref{#1}}