doc-src/springer.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.

%% $ lcp Exp $
\documentstyle[12pt,rail,proof,iman,epsf,mathsing]{book}
%\includeonly{Ref/simplifier}
%%  index{\(\w+\)\!meta-level     index{meta-\1
%%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\)    [\\ttindexbold{\1}
%% run    sedindex springer    to prepare index file

\sloppy

\title{Isabelle\\A Generic Theorem Prover}
\author{Lawrence C. Paulson\\[2ex] With Contributions by Tobias Nipkow}

\date{} 
\makeindex

\def\S{Sect.\thinspace}%This is how Springer like it

\underscoreoff

\setcounter{secnumdepth}{2} \setcounter{tocdepth}{1}

\binperiod     %%%treat . like a binary operator

\begin{document}
\maketitle

\pagenumbering{Roman}
\include{preface}

\tableofcontents
\newpage
\listoffigures
\newpage

\markboth{}{}
\newfont{\sanssi}{cmssi12}
\vspace*{2.5cm}
\begin{quote}\raggedleft
{\em To Nathan and Sarah}

\vspace*{1.2cm}
{\sanssi
You can only find truth with logic\\
if you have already found truth without it.}\\
\bigskip

G.K. Chesterton, {\em The Man who was Orthodox}
\end{quote}

\thispagestyle{empty}
\newpage
\pagenumbering{arabic}
\part{Introduction to Isabelle}   

\index{hypotheses|see{assumptions}}
\index{rewriting|see{simplification}}
\index{variables!schematic|see{unknowns}} 
\index{abstract syntax trees|see{ASTs}}

\begingroup%things local to Intro -- especially, redefining \part!!
\newcommand\qeq{\stackrel{?}{\equiv}}  %for disagreement pairs in unification
\newcommand{\nand}{\mathbin{\lnot\&}} 
\newcommand{\xor}{\mathbin{\#}}
\let\part=\chapter
\include{Intro/foundations}
\include{Intro/getting}
\include{Intro/advanced}
\endgroup

\part{The Isabelle Reference Manual} 
\include{Ref/introduction}
\include{Ref/goals}
\include{Ref/tactic}
\include{Ref/tctical}
\include{Ref/thm}
\include{Ref/theories}
\include{Ref/defining}
\include{Ref/syntax}
\include{Ref/substitution}
\include{Ref/simplifier}
\include{Ref/classical}

\part{Isabelle's Object-Logics} 
\newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
  \hrule\bigskip}
\newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}

\include{Logics/intro}
\include{Logics/FOL}
\include{Logics/ZF}
\include{Logics/HOL}
\include{Logics/LK}
\include{Logics/CTT}

\include{Ref/theory-syntax}

%%seealso's must be last so that they appear last in the index entries
\index{backtracking|seealso{{\tt back} command, search}}
\index{classes|seealso{sorts}}
\index{sorts|seealso{arities}}
\index{axioms|seealso{rules, theorems}}
\index{theorems|seealso{rules}}
\index{definitions|seealso{meta-rewriting}}
\index{equality|seealso{simplification}}

\bibliographystyle{springer} \small\raggedright\frenchspacing
\bibliography{string-abbrv,atp,funprog,general,isabelle,logicprog,theory}

\printindex
\end{document}