src/HOL/Algebra/document/root.tex
author wenzelm
Wed, 31 Dec 2008 18:53:16 +0100
changeset 29270 0eade173f77e
parent 27717 21bbd410ba04
child 35849 b5522b51cb1e
permissions -rw-r--r--
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14706
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
     1
% $Id$
13950
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
     2
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
     3
\documentclass[11pt,a4paper]{article}
14578
1f3f7e58b195 session graph;
wenzelm
parents: 14551
diff changeset
     4
\usepackage{graphicx}
13950
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
     5
\usepackage{isabelle,isabellesym}
14666
65f8680c3f16 improved notation;
wenzelm
parents: 14578
diff changeset
     6
\usepackage{amssymb}
65f8680c3f16 improved notation;
wenzelm
parents: 14578
diff changeset
     7
\usepackage[latin1]{inputenc}
65f8680c3f16 improved notation;
wenzelm
parents: 14578
diff changeset
     8
\usepackage[only,bigsqcap]{stmaryrd}
27717
21bbd410ba04 Generalised polynomial lemmas from cring to ring.
ballarin
parents: 20318
diff changeset
     9
%\usepackage{amsmath}
14666
65f8680c3f16 improved notation;
wenzelm
parents: 14578
diff changeset
    10
65f8680c3f16 improved notation;
wenzelm
parents: 14578
diff changeset
    11
% this should be the last package used
65f8680c3f16 improved notation;
wenzelm
parents: 14578
diff changeset
    12
\usepackage{pdfsetup}
65f8680c3f16 improved notation;
wenzelm
parents: 14578
diff changeset
    13
65f8680c3f16 improved notation;
wenzelm
parents: 14578
diff changeset
    14
\urlstyle{rm}
27717
21bbd410ba04 Generalised polynomial lemmas from cring to ring.
ballarin
parents: 20318
diff changeset
    15
\isabellestyle{tt}
14706
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
    16
\pagestyle{myheadings}
13950
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    17
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    18
\begin{document}
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    19
14706
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
    20
\title{The Isabelle/HOL Algebra Library}
27717
21bbd410ba04 Generalised polynomial lemmas from cring to ring.
ballarin
parents: 20318
diff changeset
    21
\author{Clemens Ballarin (Editor)}
21bbd410ba04 Generalised polynomial lemmas from cring to ring.
ballarin
parents: 20318
diff changeset
    22
\date{With contributions by Jesús Aransay, Clemens Ballarin, Stephan Hohe,
21bbd410ba04 Generalised polynomial lemmas from cring to ring.
ballarin
parents: 20318
diff changeset
    23
  Florian Kammüller and Lawrence C Paulson \\
21bbd410ba04 Generalised polynomial lemmas from cring to ring.
ballarin
parents: 20318
diff changeset
    24
  \today}
13950
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    25
\maketitle
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    26
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    27
\tableofcontents
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    28
14578
1f3f7e58b195 session graph;
wenzelm
parents: 14551
diff changeset
    29
\begin{center}
1f3f7e58b195 session graph;
wenzelm
parents: 14551
diff changeset
    30
  \includegraphics[scale=0.5]{session_graph}
1f3f7e58b195 session graph;
wenzelm
parents: 14551
diff changeset
    31
\end{center}
1f3f7e58b195 session graph;
wenzelm
parents: 14551
diff changeset
    32
1f3f7e58b195 session graph;
wenzelm
parents: 14551
diff changeset
    33
\clearpage
1f3f7e58b195 session graph;
wenzelm
parents: 14551
diff changeset
    34
27717
21bbd410ba04 Generalised polynomial lemmas from cring to ring.
ballarin
parents: 20318
diff changeset
    35
%\renewcommand{\isamarkupheader}[1]%
21bbd410ba04 Generalised polynomial lemmas from cring to ring.
ballarin
parents: 20318
diff changeset
    36
%{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
14706
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
    37
13950
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    38
\parindent 0pt\parskip 0.5ex
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    39
\input{session}
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    40
14706
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
    41
\pagestyle{headings}
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
    42
\bibliographystyle{abbrv}
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
    43
\bibliography{root}
71590b7733b7 tuned document;
wenzelm
parents: 14666
diff changeset
    44
13950
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    45
\end{document}