src/HOL/Probability/Borel_Space.thy
2014-03-18 haftmann 2014-03-18 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
2013-12-16 immler 2013-12-16 prefer box over greaterThanLessThan on euclidean_space
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-08-27 hoelzl 2013-08-27 renamed inner_dense_linorder to dense_linorder
2013-04-10 hoelzl 2013-04-10 generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
2013-03-22 hoelzl 2013-03-22 move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
2013-03-05 hoelzl 2013-03-05 generalized lemmas in Extended_Real_Limits
2013-02-13 immler 2013-02-13 eliminated union_closed_basis; cleanup Fin_Map
2013-01-14 hoelzl 2013-01-14 move prod instantiation of second_countable_topology to its definition
2013-01-14 hoelzl 2013-01-14 renamed countable_basis_space to second_countable_topology
2012-12-14 hoelzl 2012-12-14 Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
2012-12-07 hoelzl 2012-12-07 add exponential and uniform distributions
2012-12-05 hoelzl 2012-12-05 Move the measurability prover to its own file
2012-11-27 immler 2012-11-27 based countable topological basis on Countable_Set
2012-11-27 immler 2012-11-27 qualified interpretation of sigma_algebra, to avoid name clashes
2012-11-16 hoelzl 2012-11-16 move theorems to be more generally useable
2012-11-16 hoelzl 2012-11-16 more measurability rules
2012-11-16 immler 2012-11-16 allow arbitrary enumerations of basis in locale for generation of borel sets
2012-11-15 immler 2012-11-15 regularity of measures, therefore: characterization of closure with infimum distance; characterize of compact sets as totally bounded; added Diagonal_Subsequence to Library; introduced (enumerable) topological basis; rational boxes as basis of ordered euclidean space; moved some lemmas upwards
2012-11-06 hoelzl 2012-11-06 add support for function application to measurability prover
2012-11-02 hoelzl 2012-11-02 use measurability prover
2012-11-02 hoelzl 2012-11-02 add measurability prover; add support for Borel sets
2012-11-02 hoelzl 2012-11-02 add syntax and a.e.-rules for (conditional) probability on predicates
2012-10-10 hoelzl 2012-10-10 use continuity to show Borel-measurability
2012-04-25 hoelzl 2012-04-25 moved lemmas to appropriate places
2012-04-23 hoelzl 2012-04-23 reworked Probability theory
2012-03-13 wenzelm 2012-03-13 prefer abs_def over def_raw;
2012-03-12 noschinl 2012-03-12 tuned proofs
2012-02-28 wenzelm 2012-02-28 avoid undeclared variables in let bindings; tuned proofs;
2011-10-28 hoelzl 2011-10-28 correct import path
2011-10-28 hoelzl 2011-10-28 allow to build Probability and MV-Analysis with one ROOT.ML
2011-09-14 hoelzl 2011-09-14 renamed Complete_Lattices lemmas, removed legacy names
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-09-02 huffman 2011-09-02 remove more duplicate lemmas
2011-08-26 huffman 2011-08-26 make HOL-Probability respect set/pred distinction
2011-08-18 huffman 2011-08-18 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
2011-07-19 hoelzl 2011-07-19 add ereal to typeclass infinity
2011-07-19 hoelzl 2011-07-19 Rename extreal => ereal
2011-05-26 hoelzl 2011-05-26 composition of convex and measurable function is measurable
2011-05-23 hoelzl 2011-05-23 move lemmas to Extended_Reals and Extended_Real_Limits
2011-05-17 hoelzl 2011-05-17 add borel_eq_atLeastLessThan
2011-03-29 wenzelm 2011-03-29 tuned headers;
2011-03-22 hoelzl 2011-03-22 standardized headers
2011-03-14 hoelzl 2011-03-14 reworked Probability theory: measures are not type restricted to positive extended reals
2011-03-14 hoelzl 2011-03-14 moved t2_spaces to HOL image
2011-02-23 hoelzl 2011-02-23 log is borel measurable
2011-01-14 hoelzl 2011-01-14 tuned formalization of subalgebra
2010-12-08 hoelzl 2010-12-08 use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
2010-12-08 hoelzl 2010-12-08 integral over setprod
2010-12-08 haftmann 2010-12-08 work around problems with eta-expansion of equations
2010-12-08 haftmann 2010-12-08 nice syntax for lattice INFI, SUPR; various *_apply rules for lattice operations on fun; more default simplification rules
2010-12-06 hoelzl 2010-12-06 folding on arbitrary Lebesgue integrable functions
2010-12-06 hoelzl 2010-12-06 fixed spelling errors
2010-12-03 hoelzl 2010-12-03 it is known as the extended reals, not the infinite reals
2010-12-01 hoelzl 2010-12-01 Tuned setup for borel_measurable with min, max and psuminf.
2010-12-01 hoelzl 2010-12-01 Replace algebra_eqI by algebra.equality; Move sets_sigma_subset to Sigma_Algebra;
2010-12-01 hoelzl 2010-12-01 Support product spaces on sigma finite measures. Introduce the almost everywhere quantifier. Introduce 'morphism' theorems for most constants. Prove uniqueness of measures on cut stable generators. Prove uniqueness of the Radon-Nikodym derivative. Removed misleading suffix from borel_space and lebesgue_space. Use product spaces to introduce Fubini on the Lebesgue integral. Combine Euclidean_Lebesgue and Lebesgue_Measure. Generalize theorems about mutual information and entropy to arbitrary probability spaces. Remove simproc mult_log as it does not work with interpretations. Introduce completion of measure spaces. Change type of sigma. Introduce dynkin systems.