src/HOL/Probability/document/root.tex
author haftmann
Fri, 27 Jun 2025 08:09:26 +0200
changeset 82775 61c39a9e5415
parent 73595 aece5cc9efb7
permissions -rw-r--r--
typo
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}
73404
299f6a8faccc proper type-setting of cartouches (requires T1);
wenzelm
parents: 63244
diff changeset
     2
\usepackage[T1]{fontenc}
40945
b8703f63bfb2 recoded latin1 as utf8;
wenzelm
parents: 38656
diff changeset
     3
\usepackage{graphicx,isabelle,isabellesym,latexsym,textcomp}
61977
f55f28132128 proper latex setup;
wenzelm
parents: 59144
diff changeset
     4
\usepackage{amsmath}
59144
c9b75c03de3c unfortunately, there is no general function space in the measurable spaces
hoelzl
parents: 58876
diff changeset
     5
\usepackage{amssymb}
63244
af43e35211c8 import wasysym needed by Rewrite.thy
Andreas Lochbihler
parents: 61977
diff changeset
     6
\usepackage{wasysym}
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
     7
\usepackage[only,bigsqcap]{stmaryrd}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
     8
\usepackage{pdfsetup}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
     9
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    10
\urlstyle{rm}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    11
\isabellestyle{it}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    12
\pagestyle{myheadings}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    13
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    14
\begin{document}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    15
56994
8d5e5ec1cac3 fixed document generation for HOL-Probability
hoelzl
parents: 40945
diff changeset
    16
\title{Measure and Probability Theory}
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    17
\maketitle
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    18
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    19
\tableofcontents
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    20
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    21
\begin{center}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    22
  \includegraphics[scale=0.45]{session_graph}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    23
\end{center}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    24
58876
1888e3cb8048 modernized header;
wenzelm
parents: 58608
diff changeset
    25
\renewcommand{\setisabellecontext}[1]{\markright{THEORY~``#1''}}
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    26
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    27
\parindent 0pt\parskip 0.5ex
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    28
\input{session}
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    29
d5d342611edb Rewrite the Probability theory.
hoelzl
parents:
diff changeset
    30
\end{document}