20 months ago haftmann 2017-10-08 avoid name clashes on interpretation of abstract locales
22 months ago wenzelm 2017-08-18 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
2016-10-17 nipkow 2016-10-17 setprod -> prod
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-09-19 fleury 2016-09-19 left_distrib ~> distrib_right, right_distrib ~> distrib_left
2016-04-15 hoelzl 2016-04-15 fix HOL-Probability-ex
2016-02-23 nipkow 2016-02-23 more canonical names
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-13 paulson 2015-11-13 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-11-10 paulson 2015-11-10 Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
2015-09-30 paulson 2015-09-30 real_of_nat_Suc is now a simprule
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-06-19 nipkow 2015-06-19 renamed multiset_of -> mset
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-06-28 haftmann 2014-06-28 fact consolidation
2012-10-10 hoelzl 2012-10-10 simplified definitions
2012-10-10 hoelzl 2012-10-10 remove unnecessary assumption from conditional_entropy_eq
2012-04-23 hoelzl 2012-04-23 reworked Probability theory
2012-02-28 wenzelm 2012-02-28 avoid undeclared variables in let bindings; tuned proofs;
2011-12-01 hoelzl 2011-12-01 use list theorems in Dining Cryptographers and Koepf Duermuth Countermeasure
2011-12-01 hoelzl 2011-12-01 moved theorems about distribution to the definition; removed oopsed-lemma
2011-12-01 hoelzl 2011-12-01 rename finite_prob_space.setsum_distribution, it collides with prob_space.setsum_distribution
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-07-19 hoelzl 2011-07-19 Rename extreal => ereal
2011-04-05 hoelzl 2011-04-05 Rename extensional to extensionalD (extensional is also defined in FuncSet)
2011-03-14 hoelzl 2011-03-14 reworked Probability theory: measures are not type restricted to positive extended reals
2011-02-02 hoelzl 2011-02-02 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; changed syntax for simple_function, simple_integral, positive_integral, integral and RN_deriv. introduced binder variants for simple_integral, positive_integral and integral.
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
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 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.