New proof of IN_MEASURABLE_BOREL_TIMES' based on in_borel_measurable_mul

Unconditional IN_MEASURABLE_BOREL_ADD and IN_MEASURABLE_BOREL_SUB

Added extreal-based Borel measure space (ext_lborel)

Added Borel_eq_gr and Borel_eq_ge

Equivalent definitions of extreal-based Borel sets

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

Fixed tailing white-spaces and Unicode violations

Lemmas about r.v.'s having identical distribution

Attempt at better Abbrev protection

This in the face of simplification and the variable elimination done
by RW_TAC and friends. Core sequence, -t1 and some of -t2 builds (up
to category theory example).

Machinery for dynamically reverting to the old behaviours possible
through diminish_srw_ss and a trace variable.

This is work on github issue #800

Product measure and Tonelli's theorem

Replace a number of delsimps calls with temp_delsimps instead

The problem with delsimps is that it makes the change permanent for
all descendent theories.

Some proofs need adjusting as a result.

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

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

"Reverse" -> "reverse" also in CCS example

Cumulative fixes according to review comments

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

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

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`.