src/HOL/Algebra/document/root.tex
author wenzelm
Thu, 06 May 2004 14:14:18 +0200
changeset 14706 71590b7733b7
parent 14666 65f8680c3f16
child 20318 0e0ea63fe768
permissions -rw-r--r--
tuned document;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14706
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
     1
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
     2
% $Id$
13950
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
     3
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
     4
\documentclass[11pt,a4paper]{article}
14578
1f3f7e58b195 session graph;
wenzelm
parents: 14551
diff changeset
     5
\usepackage{graphicx}
13950
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
     6
\usepackage{isabelle,isabellesym}
14666
65f8680c3f16 improved notation;
wenzelm
parents: 14578
diff changeset
     7
\usepackage{amssymb}
65f8680c3f16 improved notation;
wenzelm
parents: 14578
diff changeset
     8
\usepackage[latin1]{inputenc}
65f8680c3f16 improved notation;
wenzelm
parents: 14578
diff changeset
     9
\usepackage[only,bigsqcap]{stmaryrd}
65f8680c3f16 improved notation;
wenzelm
parents: 14578
diff changeset
    10
%\usepackage{masmath}
65f8680c3f16 improved notation;
wenzelm
parents: 14578
diff changeset
    11
65f8680c3f16 improved notation;
wenzelm
parents: 14578
diff changeset
    12
% this should be the last package used
65f8680c3f16 improved notation;
wenzelm
parents: 14578
diff changeset
    13
\usepackage{pdfsetup}
65f8680c3f16 improved notation;
wenzelm
parents: 14578
diff changeset
    14
65f8680c3f16 improved notation;
wenzelm
parents: 14578
diff changeset
    15
\urlstyle{rm}
65f8680c3f16 improved notation;
wenzelm
parents: 14578
diff changeset
    16
\isabellestyle{it}
14706
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
    17
\pagestyle{myheadings}
13950
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    18
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    19
\begin{document}
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    20
14706
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
    21
\title{The Isabelle/HOL Algebra Library}
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
    22
\author{
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
    23
  Clemens Ballarin \\
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
    24
  Florian Kammu\"uller \\
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
    25
  Lawrence C Paulson \\
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
    26
}
13950
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    27
\maketitle
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    28
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    29
\tableofcontents
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    30
14578
1f3f7e58b195 session graph;
wenzelm
parents: 14551
diff changeset
    31
\begin{center}
1f3f7e58b195 session graph;
wenzelm
parents: 14551
diff changeset
    32
  \includegraphics[scale=0.5]{session_graph}
1f3f7e58b195 session graph;
wenzelm
parents: 14551
diff changeset
    33
\end{center}
1f3f7e58b195 session graph;
wenzelm
parents: 14551
diff changeset
    34
1f3f7e58b195 session graph;
wenzelm
parents: 14551
diff changeset
    35
\clearpage
1f3f7e58b195 session graph;
wenzelm
parents: 14551
diff changeset
    36
14706
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
    37
\renewcommand{\isamarkupheader}[1]%
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
    38
{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
    39
13950
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    40
\parindent 0pt\parskip 0.5ex
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    41
\input{session}
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    42
14706
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
    43
\pagestyle{headings}
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
    44
\bibliographystyle{abbrv}
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
    45
\bibliography{root}
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
    46
13950
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    47
\end{document}