src/HOL/Docs/document/root.tex
author nipkow
Wed, 11 Mar 2009 12:51:00 +0100
changeset 30442 1bc0638d554d
parent 30440 5f47d3cb781a
permissions -rw-r--r--
Added "What's in Main" to doc sources
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30440
nipkow
parents: 30401
diff changeset
     1
\documentclass[12pt,a4paper]{article}
nipkow
parents: 30401
diff changeset
     2
nipkow
parents: 30401
diff changeset
     3
\oddsidemargin=4.6mm
nipkow
parents: 30401
diff changeset
     4
\evensidemargin=4.6mm
nipkow
parents: 30401
diff changeset
     5
\textwidth=150mm
nipkow
parents: 30401
diff changeset
     6
\topmargin=4.6mm
nipkow
parents: 30401
diff changeset
     7
\headheight=0mm
nipkow
parents: 30401
diff changeset
     8
\headsep=0mm
nipkow
parents: 30401
diff changeset
     9
\textheight=234mm
nipkow
parents: 30401
diff changeset
    10
30293
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    11
\usepackage{isabelle,isabellesym}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    12
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    13
% further packages required for unusual symbols (see also
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    14
% isabellesym.sty), use only when needed
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    15
30401
nipkow
parents: 30293
diff changeset
    16
\usepackage{amssymb}
30293
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    17
  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    18
  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    19
  %\<triangleq>, \<yen>, \<lozenge>
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    20
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    21
%\usepackage[greek,english]{babel}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    22
  %option greek for \<euro>
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    23
  %option english (default language) for \<guillemotleft>, \<guillemotright>
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    24
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    25
%\usepackage[latin1]{inputenc}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    26
  %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    27
  %\<threesuperior>, \<threequarters>, \<degree>
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    28
30401
nipkow
parents: 30293
diff changeset
    29
\usepackage[only,bigsqcap]{stmaryrd}
30293
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    30
  %for \<Sqinter>
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    31
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    32
%\usepackage{eufrak}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    33
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    34
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    35
%\usepackage{textcomp}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    36
  %for \<cent>, \<currency>
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    37
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    38
% this should be the last package used
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    39
\usepackage{pdfsetup}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    40
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    41
% urls in roman style, theory text in math-similar italics
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    42
\urlstyle{rm}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    43
\isabellestyle{it}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    44
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    45
% for uniform font size
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    46
\renewcommand{\isastyle}{\isastyleminor}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    47
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    48
\parindent 0pt\parskip 0.5ex
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    49
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    50
\usepackage{supertabular}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    51
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    52
\begin{document}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    53
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    54
\title{What's in Main}
30401
nipkow
parents: 30293
diff changeset
    55
\author{Tobias Nipkow}
30442
1bc0638d554d Added "What's in Main" to doc sources
nipkow
parents: 30440
diff changeset
    56
\date{\today}
30293
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    57
\maketitle
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    58
30442
1bc0638d554d Added "What's in Main" to doc sources
nipkow
parents: 30440
diff changeset
    59
\input{Main_Doc}
30293
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    60
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    61
% optional bibliography
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    62
%\bibliographystyle{abbrv}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    63
%\bibliography{root}
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    64
cf57f2acb94c Added Docs
nipkow
parents:
diff changeset
    65
\end{document}