src/HOL/Library/document/root.tex
author wenzelm
Sun, 22 Oct 2000 22:23:16 +0200
changeset 10286 fdcdb8a80988
parent 10253 73b46b18c348
child 10674 2cc6415c1801
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]%
10286
wenzelm
parents: 10253
diff changeset
    29
{\title{***~Theory ``\isabellecontext'': unknown title}\author{}#1%
wenzelm
parents: 10253
diff changeset
    30
\ifthenelse{\equal{}{\isabelletitle}}{}{\newpage\section{\isabelletitle}}%
10253
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    31
\markright{THEORY~``\isabellecontext''}
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    32
\ifthenelse{\equal{}{\isabelleauthor}}{}%
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    33
{{\flushright\footnotesize\sl (By \isabelleauthor)\par\bigskip}}}
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    34
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    35
\parindent 0pt \parskip 0.5ex
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    36
\input{session}
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    37
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    38
\pagestyle{headings}
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    39
\bibliographystyle{abbrv}
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    40
\bibliography{root}
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    41
73b46b18c348 "The Supplemental Isabelle/HOL Library";
wenzelm
parents:
diff changeset
    42
\end{document}