doc-src/TutorialI/Documents/documents.tex

Rewrite the Probability theory.

Introduced pinfreal as real numbers with infinity.
Use pinfreal as value for measures.
Introduces Lebesgue Measure based on the integral in Multivariate Analysis.
Proved Radon Nikodym for arbitrary sigma finite measure spaces.

\chapter{Presenting Theories}
\label{ch:thy-present}

By now the reader should have become sufficiently acquainted with elementary
theory development in Isabelle/HOL\@.  The following interlude describes
how to present theories in a typographically
pleasing manner.  Isabelle provides a rich infrastructure for concrete syntax
of the underlying $\lambda$-calculus language (see
{\S}\ref{sec:concrete-syntax}), as well as document preparation of theory texts
based on existing PDF-{\LaTeX} technology (see
{\S}\ref{sec:document-preparation}).

As pointed out by Leibniz\index{Leibniz, Gottfried Wilhelm} more than 300
years ago, \emph{notions} are in principle more important than
\emph{notations}, but suggestive textual representation of ideas is vital to
reduce the mental effort to comprehend and apply them.

\input{Documents/document/Documents.tex}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: