src/HOL/Library/Library/document/root.tex
changeset 22665 cf152ff55d16
parent 22366 f4840bfffe5d
child 23101 1a05d89feeaf
equal deleted inserted replaced
22664:e965391e2864 22665:cf152ff55d16
    19 
    19 
    20 \tableofcontents
    20 \tableofcontents
    21 \newpage
    21 \newpage
    22 
    22 
    23 \renewcommand{\isamarkupheader}[1]%
    23 \renewcommand{\isamarkupheader}[1]%
    24 {\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
    24 {\ifthenelse{\equal{#1}{}}{\section{\isabellecontext}}{\section{\isabellecontext: #1}}%
       
    25 \markright{THEORY~``\isabellecontext''}}
    25 \renewcommand{\isasymguillemotright}{$\gg$}
    26 \renewcommand{\isasymguillemotright}{$\gg$}
    26 
    27 
    27 \parindent 0pt \parskip 0.5ex
    28 \parindent 0pt \parskip 0.5ex
    28 \input{session}
    29 \input{session}
    29 
    30