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