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