src/HOL/Library/Indicator_Function.thy
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.