src/HOL/Library/document/root.tex
changeset 12811 894da6aee971
parent 12810 76f3dd2f151a
child 12812 6036a579aed4
equal deleted inserted replaced
12810:76f3dd2f151a 12811:894da6aee971
     1 
       
     2 % $Id$
       
     3 
       
     4 \documentclass[11pt,a4paper]{article}
       
     5 \usepackage{ifthen}
       
     6 \usepackage{isabelle,isabellesym,pdfsetup}
       
     7 
       
     8 \urlstyle{rm}
       
     9 \isabellestyle{it}
       
    10 \pagestyle{myheadings}
       
    11 
       
    12 \begin{document}
       
    13 
       
    14 \title{The Supplemental Isabelle/HOL Library}
       
    15 \author{
       
    16   Gertrud Bauer \\
       
    17   Tobias Nipkow \\
       
    18   David von Oheimb \\
       
    19   Lawrence C Paulson \\
       
    20   Thomas M Rasmussen \\
       
    21   Christophe Tabacznyj \\
       
    22   Markus Wenzel}
       
    23 \maketitle
       
    24 
       
    25 \tableofcontents
       
    26 \newpage
       
    27 
       
    28 %now hack the "header" markup to support \title and \author
       
    29 \newcommand{\isabelletitle}{}\newcommand{\title}[1]{\gdef\isabelletitle{#1}}
       
    30 \newcommand{\isabelleauthor}{}\newcommand{\author}[1]{\gdef\isabelleauthor{#1}}
       
    31 \renewcommand{\isamarkupheader}[1]%
       
    32 {\title{***~Theory ``\isabellecontext'': unknown title}\author{}%
       
    33 #1%
       
    34 \ifthenelse{\equal{}{\isabelletitle}}{}{\newpage\section{\isabelletitle}}%
       
    35 \markright{THEORY~``\isabellecontext''}%
       
    36 \ifthenelse{\equal{}{\isabelleauthor}}{}%
       
    37 {{\flushright\footnotesize\sl (By \isabelleauthor)\par\bigskip}}}
       
    38 
       
    39 \parindent 0pt \parskip 0.5ex
       
    40 \input{session}
       
    41 
       
    42 \pagestyle{headings}
       
    43 \bibliographystyle{abbrv}
       
    44 \bibliography{root}
       
    45 
       
    46 \end{document}