src/HOL/Library/document/root.tex
author wenzelm
Thu, 14 Dec 2000 19:37:43 +0100
changeset 10674 2cc6415c1801
parent 10286 fdcdb8a80988
child 11053 026007eb2ccc
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10253
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
     1
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
     2
% $Id$
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
     3
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
     4
\documentclass[11pt,a4paper]{article}
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
     5
\usepackage{ifthen}
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
     6
\usepackage{isabelle,isabellesym,pdfsetup}
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
     7
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
     8
\urlstyle{rm}
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
     9
\isabellestyle{it}
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    10
\pagestyle{myheadings}
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    11
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    12
\begin{document}
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    13
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    14
\title{The Supplemental Isabelle/HOL Library}
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    15
\author{
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    16
  Gertrud Bauer \\
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    17
  Tobias Nipkow \\
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    18
  Lawrence C Paulson \\
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    19
  Markus Wenzel}
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    20
\maketitle
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    21
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    22
\tableofcontents
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    23
\newpage
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    24
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    25
%now hack the "header" markup to support \title and \author
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    26
\newcommand{\isabelletitle}{}\newcommand{\title}[1]{\gdef\isabelletitle{#1}}
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    27
\newcommand{\isabelleauthor}{}\newcommand{\author}[1]{\gdef\isabelleauthor{#1}}
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    28
\renewcommand{\isamarkupheader}[1]%
10674
wenzelm
parents: 10286
diff changeset
    29
{\title{***~Theory ``\isabellecontext'': unknown title}\author{}%
wenzelm
parents: 10286
diff changeset
    30
#1%
10286
wenzelm
parents: 10253
diff changeset
    31
\ifthenelse{\equal{}{\isabelletitle}}{}{\newpage\section{\isabelletitle}}%
10674
wenzelm
parents: 10286
diff changeset
    32
\markright{THEORY~``\isabellecontext''}%
10253
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    33
\ifthenelse{\equal{}{\isabelleauthor}}{}%
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    34
{{\flushright\footnotesize\sl (By \isabelleauthor)\par\bigskip}}}
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    35
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    36
\parindent 0pt \parskip 0.5ex
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    37
\input{session}
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    38
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    39
\pagestyle{headings}
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    40
\bibliographystyle{abbrv}
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    41
\bibliography{root}
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    42
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    43
\end{document}