fix a proof

Fubini's Theorem (martingaleTheory.FUBINI) + variants in some models of extreals

Product measure and Tonelli's theorem

Updated HOL Description for mathematical theories (with other cumulative fixes)

Strong Law of Large Numbers for uncorrelated r.v.'s (SLLN_uncorrelated)

Removed "Reverse" from hurdUtils, using "Tactical.reverse" instead

Radon-Nikodym Theorem for [0,+Inf]-Measure Theory (HVG concordia)

Borel and Lebesgue measure spaces (and their equivalence on Borel sets)

Equivalent definitions of `borel` from HVG's lebesgue_measureTheory;
Make real_borelTheory loadable from extreal-based probabilityTheory.

Re-defined ext_suminf (extrealTheory), only specified for positive functions;
Stop generating HTML files for probability scripts.

The new HOL-Probability based on [0,+Inf]-measure theory (#735)

* The new HOL-Probability based on [0,+Inf]-measure theory

* Noted the new HOL-Probability in next-release notes;
Added a dedicated README.md in `src/probability`.

Fix src/probability for tight equality

Remove TABs from src

Will also make selftest to check that they aren't introduced

Renamed countable_alt to upper cases

Moved COUNTABLE_ALT (as COUNTABLE_ALT_BIJ) and dependencies to pred_setTheory

Merged more countable theorems into pred_setTheory

Remove duplicated countable_def (in util_prob) and prove it as an alternative definition (countable_alt)

Use standard (>>, >-, >|) symbolic connectives for THEN*

This is done under src/, replacing Joe Hurd's earlier versions of the
same which were ++, >> and << respectively. His proofs also
occasionally rely on the fact that he made >> and >|
right-associative, which is a great idea. His symbols are inherently
bad but they clash with existing practice, and there seems to be a
good argument to trying to keep material in src reasonably
consistent. (Using >> for THEN1 instead of THEN is particularly
confusing given our current practice.)

Fix probability theories in light of pat_assum rename

Fix some theories in probability that used old-style num_case.

This is progress with github issue #97.

Delete trailing whitespace in src/

Integral on extended-real numbers [-Inf, +Inf]

Delete trailing whitespace in src/

modified prob theories according to #69

Fix src/probability's broken proof in exp kernel.

Simplify src/probability's extra_boolScript; remove examples version

Ultimate objective is to get rid of as many of these theories as
possible; the really useful theorems should just be in the original
theory under src.

Remove src/probability's redundant def'ns of THEN1 and REVERSE.

Delete src/probability's copy of BIGINTER constant; use standard one.

Updated files for version in repository

Start of work to incorporate Concordia probability theory.

Added Probability Theory