src/HOL/Limits.thy
Thu, 01 Jun 2023 12:08:33 +0100 paulson Even more material from the HOL Light metric space library
Sun, 07 May 2023 14:52:53 +0100 paulson Importation of additional lemmas from metric.ml
Tue, 07 Feb 2023 14:10:08 +0000 paulson More new theorems from the number theory development
Thu, 26 Jan 2023 13:59:51 +0000 paulson Moved in some material from the AFP entry Winding_number_eval
Wed, 21 Dec 2022 12:30:48 +0000 paulson Additional new material about infinite products, etc.
Fri, 15 Oct 2021 12:42:51 +0100 paulson A few new lemmas plus some refinements
Wed, 06 Oct 2021 14:19:46 +0200 eberlm new notion of infinite sums in HOL-Analysis, ordering on complex numbers
Mon, 28 Jun 2021 15:05:46 +0100 paulson A few useful lemmas about derivatives, colinearity and other topics
Thu, 03 Jun 2021 10:47:20 +0100 paulson new lemmas mostly about paths
Tue, 08 Sep 2020 15:30:15 +0100 paulson tidying and de-applying
Thu, 27 Aug 2020 15:23:48 +0100 paulson but not the [cong] rule
Thu, 27 Aug 2020 12:14:46 +0100 paulson tidying up some theorem statements
Wed, 13 May 2020 12:55:33 +0200 Manuel Eberl new constant power_int in HOL
Mon, 11 May 2020 11:15:41 +0100 paulson the Uniq quantifier
Tue, 26 Nov 2019 14:32:08 +0000 paulson Rearrangement of material in Complex_Analysis_Basics, which contained much that had nothing to do with complex analysis.
Sat, 02 Nov 2019 14:31:34 +0000 paulson Inverse function theorem + lemmas
Wed, 09 Oct 2019 14:51:54 +0000 haftmann dedicated fact collections for algebraic simplification rules potentially splitting goals
Wed, 09 Oct 2019 15:32:41 +0100 paulson More theorems about limits, including cancellation simprules
Wed, 09 Oct 2019 14:39:10 +0100 paulson Generalised two results concerning limits from the real numbers to type classes
Wed, 18 Sep 2019 14:41:37 +0100 paulson imported new material mostly due to Sébastien Gouëzel
Fri, 13 Sep 2019 12:46:36 +0100 paulson New theory Equivalence_Measurable_On_Borel, with the HOL Light notion of measurable_on and its equivalence to ours
Thu, 12 Sep 2019 14:51:45 +0100 paulson new material on Analysis, plus some rearrangements
Thu, 15 Aug 2019 16:11:56 +0100 paulson new material; rotated premises of Lim_transform_eventually
Wed, 17 Jul 2019 14:02:42 +0100 paulson a few new lemmas and a bit of tidying
Mon, 18 Mar 2019 15:35:34 +0000 paulson new material;' strengthened material; moved proofs out of Function_Topology in order to lessen its dependencies
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Thu, 08 Nov 2018 22:29:09 +0100 wenzelm isabelle update_cartouches -t;
Mon, 24 Sep 2018 14:30:09 +0200 nipkow Prefix form of infix with * on either side no longer needs special treatment
Thu, 30 Aug 2018 17:20:54 +0200 Manuel Eberl Some basic materials on filters and topology
Sat, 04 Aug 2018 01:03:39 +0200 eberlm Small lemmas about analysis
Wed, 11 Jul 2018 19:19:00 +0100 paulson de-applying
Wed, 11 Jul 2018 15:36:12 +0100 paulson more de-applying
Tue, 10 Jul 2018 23:18:08 +0100 paulson de-applying, etc.
Thu, 05 Jul 2018 23:37:00 +0100 paulson de-applying
Thu, 28 Jun 2018 17:14:40 +0100 paulson Incorporating new/strengthened proofs from Library and AFP entries
Sat, 26 May 2018 22:11:55 +0100 paulson tidying and reorganisation around Cauchy Integral Theorem
Wed, 02 May 2018 12:47:56 +0100 paulson type class generalisations; some work on infinite products
Wed, 28 Mar 2018 12:13:21 -0700 huffman tuned proofs and generalized some lemmas about limits
Mon, 26 Mar 2018 16:12:55 +0200 Manuel Eberl Added some simple facts about limits
Fri, 23 Feb 2018 14:56:32 +0000 Wenda Li merged
Fri, 23 Feb 2018 13:27:19 +0000 Wenda Li Unified the order of zeros and poles; improved reasoning around non-essential singularites
Thu, 22 Feb 2018 15:17:25 +0100 immler moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
Mon, 19 Feb 2018 16:44:45 +0000 paulson lots of new material, ultimately related to measure theory
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Mon, 08 Jan 2018 17:11:25 +0000 paulson moved in some material from Euler-MacLaurin
Sun, 26 Nov 2017 21:08:32 +0100 wenzelm more symbols;
Tue, 10 Oct 2017 17:15:37 +0100 paulson Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems
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;
less more (0) -100 -60 tip