src/HOL/Library/document/root.tex
author haftmann
Thu, 02 Sep 2010 10:29:48 +0200
changeset 39028 0dd6c5a0beef
parent 37848 a33ecf47f0a0
child 40945 b8703f63bfb2
permissions -rw-r--r--
use code_namespace module for SML and OCaml code
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12811
894da6aee971 moved document sources to proper place, *within* Library/Library (!);
wenzelm
parents:
diff changeset
     1
\documentclass[11pt,a4paper]{article}
894da6aee971 moved document sources to proper place, *within* Library/Library (!);
wenzelm
parents:
diff changeset
     2
\usepackage{ifthen}
12816
668073849ca9 fixed document setup of HOL-Library;
wenzelm
parents: 12811
diff changeset
     3
\usepackage[latin1]{inputenc}
26590
9114b5fe533a \usepackage[english]{babel} (required for guillemots);
wenzelm
parents: 23101
diff changeset
     4
\usepackage[english]{babel}
35795
5b95a36c1543 added stmaryrd for isasymSqinter
haftmann
parents: 31975
diff changeset
     5
\usepackage{isabelle,isabellesym,amssymb,stmaryrd}
22366
f4840bfffe5d \usepackage{amssymb};
wenzelm
parents: 21192
diff changeset
     6
\usepackage{pdfsetup}
12811
894da6aee971 moved document sources to proper place, *within* Library/Library (!);
wenzelm
parents:
diff changeset
     7
894da6aee971 moved document sources to proper place, *within* Library/Library (!);
wenzelm
parents:
diff changeset
     8
\urlstyle{rm}
894da6aee971 moved document sources to proper place, *within* Library/Library (!);
wenzelm
parents:
diff changeset
     9
\isabellestyle{it}
894da6aee971 moved document sources to proper place, *within* Library/Library (!);
wenzelm
parents:
diff changeset
    10
\pagestyle{myheadings}
894da6aee971 moved document sources to proper place, *within* Library/Library (!);
wenzelm
parents:
diff changeset
    11
894da6aee971 moved document sources to proper place, *within* Library/Library (!);
wenzelm
parents:
diff changeset
    12
\begin{document}
894da6aee971 moved document sources to proper place, *within* Library/Library (!);
wenzelm
parents:
diff changeset
    13
894da6aee971 moved document sources to proper place, *within* Library/Library (!);
wenzelm
parents:
diff changeset
    14
\title{The Supplemental Isabelle/HOL Library}
16763
14443b31ef47 moved Davenport citation to Main, removed author list
nipkow
parents: 14706
diff changeset
    15
\author{}
12811
894da6aee971 moved document sources to proper place, *within* Library/Library (!);
wenzelm
parents:
diff changeset
    16
\maketitle
894da6aee971 moved document sources to proper place, *within* Library/Library (!);
wenzelm
parents:
diff changeset
    17
894da6aee971 moved document sources to proper place, *within* Library/Library (!);
wenzelm
parents:
diff changeset
    18
\tableofcontents
894da6aee971 moved document sources to proper place, *within* Library/Library (!);
wenzelm
parents:
diff changeset
    19
\newpage
894da6aee971 moved document sources to proper place, *within* Library/Library (!);
wenzelm
parents:
diff changeset
    20
894da6aee971 moved document sources to proper place, *within* Library/Library (!);
wenzelm
parents:
diff changeset
    21
\renewcommand{\isamarkupheader}[1]%
22665
cf152ff55d16 tuned document (headers, sections, spacing);
wenzelm
parents: 22366
diff changeset
    22
{\ifthenelse{\equal{#1}{}}{\section{\isabellecontext}}{\section{\isabellecontext: #1}}%
cf152ff55d16 tuned document (headers, sections, spacing);
wenzelm
parents: 22366
diff changeset
    23
\markright{THEORY~``\isabellecontext''}}
37848
a33ecf47f0a0 bind and then latex symbols
haftmann
parents: 37118
diff changeset
    24
\newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
a33ecf47f0a0 bind and then latex symbols
haftmann
parents: 37118
diff changeset
    25
\newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}}
12811
894da6aee971 moved document sources to proper place, *within* Library/Library (!);
wenzelm
parents:
diff changeset
    26
894da6aee971 moved document sources to proper place, *within* Library/Library (!);
wenzelm
parents:
diff changeset
    27
\input{session}
894da6aee971 moved document sources to proper place, *within* Library/Library (!);
wenzelm
parents:
diff changeset
    28
894da6aee971 moved document sources to proper place, *within* Library/Library (!);
wenzelm
parents:
diff changeset
    29
\pagestyle{headings}
894da6aee971 moved document sources to proper place, *within* Library/Library (!);
wenzelm
parents:
diff changeset
    30
\bibliographystyle{abbrv}
894da6aee971 moved document sources to proper place, *within* Library/Library (!);
wenzelm
parents:
diff changeset
    31
\bibliography{root}
894da6aee971 moved document sources to proper place, *within* Library/Library (!);
wenzelm
parents:
diff changeset
    32
894da6aee971 moved document sources to proper place, *within* Library/Library (!);
wenzelm
parents:
diff changeset
    33
\end{document}