| #
c0ca1d19 |
|
28-May-2020 |
Chun Tian <binghe.lisp@gmail.com> |
Product measure and Tonelli's theorem
|
| #
486e9658 |
|
11-Apr-2020 |
Chun Tian (binghe) <binghe.lisp@gmail.com> |
Updated HOL Description for mathematical theories (with other cumulative fixes)
|
| #
0a7939af |
|
31-Jan-2020 |
Chun Tian (binghe) <binghe.lisp@gmail.com> |
Borel and Lebesgue measure spaces (and their equivalence on Borel sets)
|
| #
c4db120b |
|
19-Sep-2019 |
Chun Tian <binghe.lisp@gmail.com> |
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`.
|
| #
c487306c |
|
16-Sep-2019 |
Chun Tian (binghe) <binghe.lisp@gmail.com> |
Removed iterateTheory.inf', added inf_alt (alternative definition)
|
| #
a4c3ac80 |
|
16-Sep-2019 |
Chun Tian (binghe) <binghe.lisp@gmail.com> |
Fixed duplicated definition of "inf" in iterateTheory
|
| #
35879111 |
|
18-Aug-2019 |
Chun Tian <binghe.lisp@gmail.com> |
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
|
| #
81a09c5c |
|
01-May-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix src/probability for tight equality
|
| #
1fbad939 |
|
21-Oct-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove TABs from source files (and some trailing w/space)
|
| #
c9dac5da |
|
10-Sep-2018 |
Chun Tian (binghe) <binghe.lisp@gmail.com> |
Stage work on moving hol-light's cardinal theorems into HOL4's cardinalTheory
|
| #
9420ca26 |
|
10-Sep-2018 |
Chun Tian (binghe) <binghe.lisp@gmail.com> |
Moved hol-light's wellorder theorems into HOL4's wellorderTheory
|
| #
8df6b672 |
|
10-Sep-2018 |
Chun Tian (binghe) <binghe.lisp@gmail.com> |
Stage work on moving hol-light's cardinal theorems into HOL4's cardinalTheory
|
| #
345d397b |
|
09-Sep-2018 |
Chun Tian (binghe) <binghe.lisp@gmail.com> |
Removed/renamed duplicated theorems in rich_cardinalTheory with pred_setTheory
|
| #
0541b543 |
|
07-Sep-2018 |
Chun Tian (binghe) <binghe.lisp@gmail.com> |
Fixed a theory's name (CARD_DISJOINT_UNION)
|
| #
f5bd5abc |
|
07-Sep-2018 |
Chun Tian (binghe) <binghe.lisp@gmail.com> |
Merged hol-light's cardTheory (rich_cardinalTheory) with HOL4's cardinalTheory
|
| #
8f627d12 |
|
27-Aug-2018 |
Chun Tian (binghe) <binghe.lisp@gmail.com> |
Merged HOL4's original topologyTheory with HOL-light's version
|
| #
7f94f460 |
|
22-Aug-2018 |
Chun Tian (binghe) <binghe.lisp@gmail.com> |
Added rich_topologyTheory and dependents
|