src/HOL/Library/Indicator_Function.thy
2017-01-29 wenzelm 2017-01-29 added inj_def (redundant, analogous to surj_def, bij_def); tuned proofs;
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-09-29 hoelzl 2016-09-29 HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
2016-08-10 wenzelm 2016-08-10 tuned proofs;
2016-06-16 wenzelm 2016-06-16 tuned;
2016-05-17 eberlm 2016-05-17 Moved material from AFP/Randomised_Social_Choice to distribution
2016-05-13 wenzelm 2016-05-13 eliminated use of empty "assms";
2016-03-17 hoelzl 2016-03-17 more stuff for extended nonnegative real numbers
2016-02-23 nipkow 2016-02-23 more canonical names
2015-12-29 wenzelm 2015-12-29 more symbols;
2015-12-28 wenzelm 2015-12-28 more symbols;
2015-11-11 Andreas Lochbihler 2015-11-11 add lemmas
2015-06-26 wenzelm 2015-06-26 tuned whitespace;
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2014-11-14 hoelzl 2014-11-14 cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-10-20 hoelzl 2014-10-20 add tendsto_const and tendsto_ident_at as simp and intro rules
2014-06-30 hoelzl 2014-06-30 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
2014-06-30 hoelzl 2014-06-30 some lemmas about the indicator function; removed lemma sums_def2
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-05-19 hoelzl 2014-05-19 introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
2013-11-12 hoelzl 2013-11-12 equation when indicator function equals 0 or 1
2011-11-09 wenzelm 2011-11-09 avoid inconsistent sort constraints;
2010-07-01 hoelzl 2010-07-01 Add theory for indicator function.