Added in_borel_measurable_sqr and in_borel_measurable_mul (real_borelTheory)

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

Simplified THREE_SETS_INTER and changed it to a local lemma (used only once)

Elementary "conditional probability" (and Bayes' rule, etc.) from HVG's cond_probTheory

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.

Henstock–Kurzweil integral (ported from HOL Light)

Fixed real_topologyTheory for tight equality

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

Tactic to automate some routine set theory by reduction to FOL (#722)

* Moved SET_TAC into pred_setLib; some additions in pred_set and real theories

* Added quantifiers to COUNT_11

* Added missing "from_def" and related theorems (moved from real_topology to util_prob)

* Renamed SET_RULE to SET_CONV

* Added util_probTheory (from_def) into dependencies of real_topologyTheory

* Cancel changes in seqTheory

* Cancelled SUBSET_DIFF_DISJOINT and SUBSET_BIGUNION

* Further canceled two "tail_*" theorems

* IMAGE_EMPTY_FUN -> IMAGE_CONST (more general)

* Canceled IMAGE_EMPTY_FUN/IMAGE_CONST (IMAGE_EQ_SING is more general)

* Moved SET_TAC, ASM_SET_TAC and SET_RULE to bossLib with documentation (help and release notes)

* Reverted (original) empty lines in pred_setLib files

Fix src/probability for tight equality

Remove TABs from source files (and some trailing w/space)

Added rich_topologyTheory and dependents

Remove TABs from src

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

More additions in pred_set and util_probTheory

Removed version 2 of measure & probabilityTheory

Additional theorems about "minimal" in util_probTheory

Removed right-associative THEN and THEN1 in extreal and util_probScript

Move BIJ_FINITE_SUBSET and IMAGE_II from util_prob to pred_setTheory

Move basic PREIMAGE lemmas from util_prob to pred_setTheory

Moved FINITE_BIJ and BIJ_ALT to pred_setTheory

Moved COUNTABLE_ALT (as COUNTABLE_ALT_BIJ) and dependencies to pred_setTheory

Removed some duplicated countable theorems from util_probTheory

Merged more countable theorems into pred_setTheory

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

Move Schroeder-Bernstein theorem (and related settings) to pred_setTheory (from util_prob):

SUBSET_THM
K_SUBSET
SUBSET_K
FUNSET
DFUNSET
IN_FUNSET
IN_DFUNSET
FUNSET_THM
UNIV_FUNSET_UNIV
FUNSET_DFUNSET
EMPTY_FUNSET
FUNSET_EMPTY
FUNSET_INTER
schroeder_close
SCHROEDER_CLOSE
SCHROEDER_CLOSED
SCHROEDER_CLOSE_SUBSET
SCHROEDER_CLOSE_SET
SCHROEDER_BERNSTEIN_AUTO
SCHROEDER_BERNSTEIN
BIJ_INJ_SURJ

Moved 23 small theorems from util_prob to pred_setTheory:

BIGINTER_SUBSET
BIGUNION_IMAGE_UNIV
BIJ_SYM
BIJ_SYM_IMP
BIJ_TRANS
DIFF_BIGINTER
DIFF_INTER
DIFF_INTER2
DISJOINT_ALT
DISJOINT_COUNT
DISJOINT_DIFF
DISJOINT_DIFFS
EQ_SUBSET_SUBSET
FINITE_REST_EQ
INFINITE_INJ
INJ_IMAGE_BIJ
IN_BIGINTER_IMAGE
IN_BIGUNION_IMAGE
IN_EQ_UNIV_IMP
SUBSET_ADD
SUBSET_INTER1
SUBSET_INTER2
SURJ_IMP_INJ

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

Remove some duplicates of the theorem TRUTH.

These are:
• INFINITE_DEF and IN_LIST_TO_SET (replaced with overloadings)
• IN_APP_applied and IN_ABS_applied (inadvertently generated)

Also, made changes to try to avoid new definitions in listTheory accidentally having a "_DEF" suffix instead of "_def". Old naming inconsistencies still remain in listTheory (e.g. EXISTS_DEF, FIND_def and FLAT).

These changes will break a few proofs but patches should be trivial (i.e. removing references to these TRUTH theorems and/ or renaming "_DEF" to "_def").

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/

extra theories no longer needed. some of the theorems were moved to src/probability/util_prob. Ref #69