| #
a4784f6f |
|
09-Oct-2019 |
haftmann <none@none> |
dedicated fact collections for algebraic simplification rules potentially splitting goals
--HG--
extra : rebase_source : ebbd8d0c13409f8fb536c42910e904c24e43dbe6
|
| #
b15d33eb |
|
13-Apr-2018 |
paulson <lp15@cam.ac.uk> |
Probability builds with new definitions
|
| #
c260d507 |
|
20-Feb-2018 |
wenzelm <none@none> |
tuned proofs -- prefer explicit names for facts from 'interpret';
|
| #
c2d49d41 |
|
17-Aug-2017 |
eberlm <eberlm@in.tum.de> |
Replaced subseq with strict_mono
|
| #
246d8de3 |
|
28-Feb-2017 |
paulson <lp15@cam.ac.uk> |
Renamed ii to imaginary_unit in order to free up ii as a variable name. Also replaced some legacy def commands
|
| #
334e78e7 |
|
17-Oct-2016 |
hoelzl <none@none> |
HOL-Analysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
--HG--
extra : rebase_source : 081106cd39425dcfe6a04e687466bbb9ffedb25e
|
| #
a1e8064f |
|
13-Oct-2016 |
hoelzl <none@none> |
HOL-Probability: move conditional expectation from AFP/Ergodic_Theory
--HG--
extra : rebase_source : 55f4bbfc342a2532835d5bd35b92dd5cf39bc512
|
| #
78a9e4a8 |
|
16-Sep-2016 |
hoelzl <none@none> |
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
--HG--
extra : rebase_source : 0321297c249a436ca0371010a76a1a026dd33222
|
| #
eb030641 |
|
02-Aug-2016 |
wenzelm <none@none> |
more symbols;
|
| #
14001a0d |
|
22-Jul-2016 |
wenzelm <none@none> |
tuned proofs -- avoid unstructured calculation;
|
| #
ea4763a3 |
|
05-Jul-2016 |
hoelzl <none@none> |
Probability: simplified Levy's uniqueness theorem
--HG--
extra : rebase_source : 55fccc244e711a09badda8e8ecf9735e18696a83
|
| #
7baf2986 |
|
13-Jun-2016 |
hoelzl <none@none> |
Probability: tuned headers; cleanup Radon_Nikodym
--HG--
extra : rebase_source : b1923775a469aec44566a1d1da6c9d6e69cb0de4
|
| #
66281660 |
|
26-May-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
79d3be54 |
|
14-Apr-2016 |
hoelzl <none@none> |
Probability: move emeasure and nn_integral from ereal to ennreal
--HG--
extra : rebase_source : 5f2ac8a84abb43927a58086db8bbe10e190b2e77
|
| #
15ee6658 |
|
24-Feb-2016 |
paulson <lp15@cam.ac.uk> |
Substantial new material for multivariate analysis. Also removal of some duplicates.
|
| #
5ad25152 |
|
05-Jan-2016 |
hoelzl <none@none> |
add the proof of the central limit theorem
--HG--
extra : rebase_source : 493d99e28392771c51f4102a11b90533880e289f
extra : amend_source : 3fb7b7c607104e57a2c3ba7f733dd570eb42fa3b
|