src/HOL/document/root.tex
changeset 72860 65554bac121b
parent 61977 f55f28132128
child 73656 299f6a8faccc
equal deleted inserted replaced
72859:429afd0d1a79 72860:65554bac121b
    26 \newpage
    26 \newpage
    27 
    27 
    28 \renewcommand{\setisabellecontext}[1]{\markright{THEORY~``#1''}}
    28 \renewcommand{\setisabellecontext}[1]{\markright{THEORY~``#1''}}
    29 
    29 
    30 \parindent 0pt\parskip 0.5ex
    30 \parindent 0pt\parskip 0.5ex
       
    31 \input{Code_Generator.tex}
    31 \input{session}
    32 \input{session}
    32 
    33 
    33 \pagestyle{headings}
    34 \pagestyle{headings}
    34 \bibliographystyle{abbrv}
    35 \bibliographystyle{abbrv}
    35 \bibliography{root}
    36 \bibliography{root}