src/HOL/Library/Liminf_Limsup.thy
Thu, 18 Jul 2019 14:08:28 +0100 paulson more new material about analysis
Tue, 05 Mar 2019 07:00:21 +0000 haftmann avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
Mon, 14 Jan 2019 18:35:03 +0000 haftmann tuned proofs
Sun, 18 Nov 2018 18:07:51 +0000 haftmann removed legacy input syntax
Thu, 08 Nov 2018 09:11:52 +0100 haftmann removed relics of ASCII syntax for indexed big operators
Thu, 30 Aug 2018 17:20:54 +0200 Manuel Eberl Some basic materials on filters and topology
Thu, 17 Aug 2017 14:52:56 +0200 eberlm Replaced subseq with strict_mono
Thu, 15 Sep 2016 16:07:20 +0200 immler Liminf/Limsup and filtermap
Thu, 14 Apr 2016 15:48:11 +0200 hoelzl Probability: move emeasure and nn_integral from ereal to ennreal
Wed, 16 Mar 2016 11:49:56 +0100 hoelzl generalized some Borel measurable statements to support ennreal
Wed, 17 Feb 2016 21:51:56 +0100 haftmann prefer abbreviations for compound operators INFIMUM and SUPREMUM
Mon, 04 Jan 2016 17:45:36 +0100 eberlm Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
Wed, 30 Dec 2015 11:21:54 +0100 wenzelm more symbols;
Tue, 29 Dec 2015 23:04:53 +0100 wenzelm more symbols;
Thu, 17 Dec 2015 16:43:36 +0100 hoelzl moved some theorems from the CLT proof; reordered some theorems / notation
less more (0) -15 tip