src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
Tue, 27 Sep 2016 16:24:53 +0100 paulson a few new theorems and a renaming
Mon, 26 Sep 2016 16:57:05 +0200 hoelzl use filter to define Henstock-Kurzweil integration
Fri, 23 Sep 2016 18:34:34 +0200 hoelzl move absolutely_integrable_on to Equivalence_Lebesgue_Henstock_Integration, now based on the Lebesgue integral
Fri, 23 Sep 2016 10:26:04 +0200 hoelzl prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
Thu, 22 Sep 2016 15:44:47 +0100 paulson More mainly topological results
Wed, 21 Sep 2016 16:59:51 +0100 paulson new material about topological concepts, etc
Mon, 19 Sep 2016 20:06:21 +0200 fleury left_distrib ~> distrib_right, right_distrib ~> distrib_left
Fri, 16 Sep 2016 13:56:51 +0200 hoelzl move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
Thu, 25 Aug 2016 15:50:43 +0200 Manuel Eberl More analysis lemmas
Fri, 12 Aug 2016 17:53:55 +0200 wenzelm more symbols;
Wed, 10 Aug 2016 18:57:20 +0200 haftmann keeping lifting rules local
Mon, 08 Aug 2016 14:13:14 +0200 hoelzl rename HOL-Multivariate_Analysis to HOL-Analysis.
less more (0) tip