src/HOL/Algebra/document/root.tex
author ballarin
Tue, 13 Apr 2004 09:42:40 +0200
changeset 14551 2cb6ff394bfb
parent 13950 74f638d8a829
child 14578 1f3f7e58b195
permissions -rw-r--r--
Various changes to HOL-Algebra; Locale instantiation.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13950
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
     1
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
     2
\documentclass[11pt,a4paper]{article}
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
     3
\usepackage{isabelle,isabellesym}
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
     4
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
     5
%\usepackage{substr}
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
     6
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
     7
%\renewcommand{\isamarkupheader}[1]{%
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
     8
%  \IfSubStringInString{Chapter: }{#1}{%
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
     9
%    \chapter{\BehindSubString{Chapter: }{#1}}}{%
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    10
%  \section{#1}}}
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    11
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    12
% further packages required for unusual symbols (see also isabellesym.sty)
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    13
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    14
%\usepackage{latexsym}                 % for \<leadsto>, \<box>, \<diamond>,
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    15
                                       %   \<sqsupset>, \<mho>, \<Join>
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    16
                                       %   and \<lhd> and others!
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    17
\usepackage{amssymb}                  % for \<lesssim>, \<greatersim>,
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    18
                                       %   \<lessapprox>, \<greaterapprox>,
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    19
                                       %   \<triangleq>, \<yen>, \<lozenge>
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    20
%\usepackage[english]{babel}           % for \<guillemotleft> \<guillemotright>
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    21
\usepackage[latin1]{inputenc}         % for \<onesuperior>, \<onequarter>,
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    22
                                       %   \<twosuperior>, \<onehalf>,
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    23
                                       %   \<threesuperior>, \<threequarters>
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    24
                                       %   \<degree>
14551
2cb6ff394bfb Various changes to HOL-Algebra;
ballarin
parents: 13950
diff changeset
    25
\usepackage[only,bigsqcap]{stmaryrd}  % for \<Sqinter>
13950
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    26
%\usepackage{wasysym}
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    27
%\usepackage{eufrak}                   % for \<AA> ... \<ZZ>, \<aa> ... \<zz>
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    28
%\usepackage{textcomp}                  % for \<zero> ... \<nine>, \<cent>
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    29
                                       %   \<currency>
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    30
%\usepackage{marvosym}                 % for \<euro>
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    31
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    32
% this should be the last package used
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    33
\usepackage{pdfsetup}
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    34
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    35
% proper setup for best-style documents
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    36
\urlstyle{rm}
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    37
\isabellestyle{it}
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    38
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    39
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    40
\begin{document}
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    41
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    42
\title{The Isabelle Algebra Library}
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    43
\maketitle
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    44
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    45
\tableofcontents
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    46
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    47
\parindent 0pt\parskip 0.5ex
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    48
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    49
% include generated text of all theories
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    50
\input{session}
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    51
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    52
%\bibliographystyle{abbrv}
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    53
%\bibliography{root}
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    54
74f638d8a829 File for document preparation.
ballarin
parents:
diff changeset
    55
\end{document}