History log of /seL4-l4v-master/isabelle/src/HOL/Probability/Distribution_Functions.thy
Revision Date Author Comments
# 97b2ecf5 08-Nov-2018 haftmann <none@none>

removed relics of ASCII syntax for indexed big operators


# 1394cb87 28-Jun-2018 paulson <lp15@cam.ac.uk>

Incorporating new/strengthened proofs from Library and AFP entries


# bbbbfe22 20-Oct-2016 hoelzl <none@none>

HOL-Probability: generalize theorems about cumulative distribution function


# 05ddf657 02-Oct-2016 wenzelm <none@none>

updated headers;


# c4a680cf 30-Sep-2016 hoelzl <none@none>

HOL-Analysis: move Continuum_Not_Denumerable from Library

--HG--
rename : src/HOL/Library/Continuum_Not_Denumerable.thy => src/HOL/Analysis/Continuum_Not_Denumerable.thy


# c054b489 12-Jul-2016 wenzelm <none@none>

more standard name;

--HG--
rename : src/HOL/Library/ContNotDenum.thy => src/HOL/Library/Continuum_Not_Denumerable.thy


# 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;


# 1daf8189 13-May-2016 wenzelm <none@none>

eliminated use of empty "assms";


# 79d3be54 14-Apr-2016 hoelzl <none@none>

Probability: move emeasure and nn_integral from ereal to ennreal

--HG--
extra : rebase_source : 5f2ac8a84abb43927a58086db8bbe10e190b2e77


# 5ad25152 05-Jan-2016 hoelzl <none@none>

add the proof of the central limit theorem

--HG--
extra : rebase_source : 493d99e28392771c51f4102a11b90533880e289f
extra : amend_source : 3fb7b7c607104e57a2c3ba7f733dd570eb42fa3b