src/HOL/Filter.thy
Sun, 07 May 2023 14:52:53 +0100 paulson Importation of additional lemmas from metric.ml
Thu, 16 Feb 2023 10:42:28 +0000 paulson New material due to Eberl on Formal Laurent Series
Wed, 08 Feb 2023 15:05:24 +0000 paulson Lots of new material chiefly about complex analysis
Tue, 07 Feb 2023 14:10:08 +0000 paulson More new theorems from the number theory development
Tue, 31 Jan 2023 14:05:16 +0000 paulson Lots more new material thanks to Manuel Eberl
Tue, 20 Dec 2022 17:59:44 +0000 paulson First round of moving material from the number theory development
Mon, 20 Sep 2021 13:52:09 +0200 wenzelm tuned proofs --- eliminated 'guess';
Fri, 10 Apr 2020 22:50:59 +0100 paulson more removal of applys
Wed, 23 Oct 2019 16:09:23 +0000 haftmann tuned syntax
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Sat, 10 Nov 2018 07:57:19 +0000 haftmann clarified status of legacy input abbreviations
Thu, 08 Nov 2018 22:29:09 +0100 wenzelm isabelle update_cartouches -t;
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
Fri, 20 Jul 2018 10:09:59 +0200 Andreas Lochbihler add lemmas about prod_filter
Wed, 28 Mar 2018 11:19:07 -0700 huffman tuned some proofs about filters
Mon, 26 Mar 2018 16:12:55 +0200 Manuel Eberl Added some simple facts about limits
Wed, 14 Mar 2018 15:08:46 +0100 wenzelm misc tuning and clarification;
Fri, 23 Feb 2018 13:27:19 +0000 Wenda Li Unified the order of zeros and poles; improved reasoning around non-essential singularites
Fri, 16 Feb 2018 10:59:14 +0100 Andreas Lochbihler strengthen filter relator to canonical categorical definition with better properties
Thu, 15 Feb 2018 12:11:00 +0100 wenzelm more symbols;
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Fri, 23 Jun 2017 13:16:04 +0200 eberlm distrib_lattice instance for filters
Thu, 22 Jun 2017 10:50:18 +0200 eberlm Contravariant map on filters
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, 30 Sep 2016 14:05:51 +0100 paulson new material on paths, etc. Also rationalisation
Thu, 28 Jul 2016 17:16:16 +0200 immler numerical bounds on pi
Fri, 22 Jul 2016 11:00:43 +0200 wenzelm tuned proofs -- avoid unstructured calculation;
Wed, 22 Jun 2016 10:09:20 +0200 wenzelm bundle lifting_syntax;
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!
Fri, 19 Feb 2016 13:40:50 +0100 hoelzl generalize more theorems to support enat and ennreal
Tue, 09 Feb 2016 06:39:31 +0100 hoelzl instantiate topologies for nat, int and enat
Mon, 08 Feb 2016 17:18:13 +0100 hoelzl move product topology to HOL-Complex_Main
Wed, 17 Feb 2016 21:51:56 +0100 haftmann prefer abbreviations for compound operators INFIMUM and SUPREMUM
Mon, 11 Jan 2016 11:56:35 +0100 hoelzl setup code generation for filters as suggested by Florian
Fri, 08 Jan 2016 17:41:04 +0100 hoelzl fix code generation for uniformity: uniformity is a non-computable pure data.
Fri, 08 Jan 2016 17:40:59 +0100 hoelzl add uniform spaces
Mon, 28 Dec 2015 21:47:32 +0100 wenzelm former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
Mon, 28 Dec 2015 18:03:26 +0100 wenzelm use symbols by default;
Sun, 13 Dec 2015 21:56:15 +0100 wenzelm more general types Proof.method / context_tactic;
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, 02 Nov 2015 11:56:28 +0100 eberlm Rounding function, uniform limits, cotangent, binomial identities
Fri, 09 Oct 2015 20:26:03 +0200 wenzelm discontinued specific HTML syntax;
Fri, 25 Sep 2015 16:54:31 +0200 hoelzl prove Liminf_inverse_ereal
Tue, 22 Sep 2015 16:53:59 +0100 paulson Prepared two non-terminating proofs; no obvious link with my changes
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;
Sat, 18 Jul 2015 20:47:08 +0200 wenzelm prefer tactics with explicit context;
Tue, 14 Jul 2015 13:48:03 +0200 hoelzl generalized filtermap_homeomorph to filtermap_fun_inverse; add eventually_at_top/bot_not_equal
Fri, 26 Jun 2015 14:53:28 +0200 wenzelm do not expose goal parameters;
Thu, 07 May 2015 15:34:28 +0200 hoelzl generalized tends over powr; added DERIV rule for powr
Sun, 12 Apr 2015 11:34:09 +0200 hoelzl move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
Sun, 12 Apr 2015 11:33:50 +0200 hoelzl add cofinite filter
Sun, 12 Apr 2015 11:33:44 +0200 hoelzl add frequently as dual for eventually
Sun, 12 Apr 2015 11:33:30 +0200 hoelzl add quantifier syntax for eventually
Sun, 12 Apr 2015 11:33:19 +0200 hoelzl move filters to their own theory
less more (0) tip