src/HOL/Limits.thy
Mon, 09 Oct 2017 15:34:23 +0100 paulson new material about connectedness, etc.
Sun, 20 Aug 2017 03:35:20 +0200 Manuel Eberl Various lemmas for HOL-Analysis
Thu, 17 Aug 2017 14:52:56 +0200 eberlm Replaced subseq with strict_mono
Tue, 02 May 2017 14:34:06 +0100 paulson Simplification of some proofs. Also key lemmas using !! rather than ! in premises
Tue, 25 Apr 2017 16:39:54 +0100 paulson New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
Fri, 10 Mar 2017 23:16:40 +0100 immler modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
Tue, 21 Feb 2017 15:04:01 +0000 paulson Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion
Tue, 25 Oct 2016 15:46:07 +0100 paulson more new material
Tue, 18 Oct 2016 15:55:53 +0100 paulson more from moretop.ml
Mon, 17 Oct 2016 17:33:07 +0200 nipkow setprod -> prod
Mon, 17 Oct 2016 11:46:22 +0200 nipkow setsum -> sum
Wed, 28 Sep 2016 17:01:01 +0100 paulson new material connected with HOL Light measure theory, plus more rationalisation
Sun, 18 Sep 2016 20:33:48 +0200 wenzelm tuned proofs;
Thu, 25 Aug 2016 15:50:43 +0200 Manuel Eberl More analysis lemmas
Thu, 28 Jul 2016 17:16:16 +0200 immler numerical bounds on pi
Mon, 25 Jul 2016 14:02:29 +0200 wenzelm unused (see 1e9e68247ad1);
Fri, 22 Jul 2016 23:55:47 +0200 wenzelm misc tuning and modernization;
Tue, 14 Jun 2016 15:34:21 +0100 paulson new results about topology
Thu, 09 Jun 2016 16:04:20 +0200 immler approximation, derivative, and continuity of floor and ceiling
Fri, 20 May 2016 21:21:28 +0200 immler reduce isUCont to uniformly_continuous_on
Wed, 11 May 2016 16:13:17 +0200 immler introduced class topological_group between topological_monoid and real_normed_vector
Mon, 25 Apr 2016 16:09:26 +0200 wenzelm eliminated old 'def';
Tue, 23 Feb 2016 18:04:31 +0100 nipkow resolved conflict
Tue, 23 Feb 2016 16:25:08 +0100 nipkow more canonical names
Tue, 23 Feb 2016 15:47:39 +0000 paulson New and revised material for (multivariate) analysis
Mon, 22 Feb 2016 14:37:56 +0000 paulson An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
Tue, 09 Feb 2016 06:39:31 +0100 hoelzl instantiate topologies for nat, int and enat
Mon, 08 Feb 2016 19:53:49 +0100 hoelzl add type class for topological monoids
Fri, 08 Jan 2016 17:40:59 +0100 hoelzl add uniform spaces
Thu, 07 Jan 2016 17:40:55 +0000 paulson revisions to limits and derivatives, plus new lemmas
Wed, 30 Dec 2015 14:05:51 +0100 wenzelm more symbols;
Wed, 30 Dec 2015 11:21:54 +0100 wenzelm more symbols;
Tue, 29 Dec 2015 23:04:53 +0100 wenzelm more symbols;
Wed, 23 Dec 2015 14:36:45 +0100 immler transfer rule for bounded_linear of blinfun
Wed, 09 Dec 2015 17:35:22 +0000 paulson sorted out eventually_mono
Mon, 07 Dec 2015 16:44:26 +0000 paulson Cauchy's integral formula for circles. Starting to fix eventually_mono.
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Mon, 23 Nov 2015 16:57:54 +0000 paulson New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
Tue, 17 Nov 2015 12:32:08 +0000 paulson Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
Fri, 13 Nov 2015 12:27:13 +0000 paulson Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
Tue, 10 Nov 2015 14:18:41 +0000 paulson Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
Mon, 02 Nov 2015 16:17:09 +0100 eberlm Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
Mon, 02 Nov 2015 11:56:28 +0100 eberlm Rounding function, uniform limits, cotangent, binomial identities
Thu, 29 Oct 2015 15:40:52 +0100 eberlm added many small lemmas about setsum/setprod/powr/...
Sun, 13 Sep 2015 22:56:52 +0200 wenzelm tuned proofs -- less legacy;
Tue, 01 Sep 2015 22:32:58 +0200 wenzelm eliminated \<Colon>;
Wed, 19 Aug 2015 19:18:19 +0100 paulson New material and fixes related to the forthcoming Stone-Weierstrass development
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Tue, 14 Jul 2015 13:48:03 +0200 hoelzl generalized filtermap_homeomorph to filtermap_fun_inverse; add eventually_at_top/bot_not_equal
Thu, 07 May 2015 15:34:28 +0200 hoelzl generalized tends over powr; added DERIV rule for powr
Tue, 21 Apr 2015 17:19:00 +0100 paulson New material, mostly about limits. Consolidation.
Sat, 11 Apr 2015 11:56:40 +0100 paulson Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
Tue, 31 Mar 2015 21:54:32 +0200 haftmann given up separate type classes demanding `inverse 0 = 0`
Thu, 05 Mar 2015 17:30:29 +0000 paulson The function frac. Various lemmas about limits, series, the exp function, etc.
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Mon, 20 Oct 2014 18:33:14 +0200 hoelzl add tendsto_const and tendsto_ident_at as simp and intro rules
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
Mon, 30 Jun 2014 15:45:21 +0200 hoelzl import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
Wed, 18 Jun 2014 14:31:32 +0200 hoelzl filters are easier to define with INF on filters.
Wed, 18 Jun 2014 07:31:12 +0200 hoelzl moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
less more (0) -100 -60 tip