src/HOL/Probability/document/root.tex
author wenzelm
Fri, 23 Mar 2018 17:09:36 +0100
changeset 67933 604da273e18d
parent 63244 af43e35211c8
child 73404 299f6a8faccc
permissions -rw-r--r--
more robust timing info: do not rely on order of markup;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
     1
\documentclass[11pt,a4paper]{article}
40945
b8703f63bfb2 recoded latin1 as utf8;
wenzelm
parents: 38656
diff changeset
     2
\usepackage{graphicx,isabelle,isabellesym,latexsym,textcomp}
61977
f55f28132128 proper latex setup;
wenzelm
parents: 59144
diff changeset
     3
\usepackage{amsmath}
59144
c9b75c03de3c unfortunately, there is no general function space in the measurable spaces
hoelzl
parents: 58876
diff changeset
     4
\usepackage{amssymb}
63244
af43e35211c8 import wasysym needed by Rewrite.thy
Andreas Lochbihler
parents: 61977
diff changeset
     5
\usepackage{wasysym}
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
     6
\usepackage[only,bigsqcap]{stmaryrd}
40945
b8703f63bfb2 recoded latin1 as utf8;
wenzelm
parents: 38656
diff changeset
     7
\usepackage[utf8]{inputenc}
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
     8
\usepackage{pdfsetup}
58608
5b7f0b5da884 fix document generation for HOL-Probability
hoelzl
parents: 56994
diff changeset
     9
\usepackage[english]{babel}
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    10
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    11
\urlstyle{rm}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    12
\isabellestyle{it}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    13
\pagestyle{myheadings}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    14
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    15
\begin{document}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    16
56994
8d5e5ec1cac3 fixed document generation for HOL-Probability
hoelzl
parents: 40945
diff changeset
    17
\title{Measure and Probability Theory}
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    18
\maketitle
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    19
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    20
\tableofcontents
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    21
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    22
\begin{center}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    23
  \includegraphics[scale=0.45]{session_graph}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    24
\end{center}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    25
58876
1888e3cb8048 modernized header;
wenzelm
parents: 58608
diff changeset
    26
\renewcommand{\setisabellecontext}[1]{\markright{THEORY~``#1''}}
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    27
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    28
\parindent 0pt\parskip 0.5ex
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    29
\input{session}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    30
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    31
\end{document}