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