src/HOL/Limits.thy
22 months ago paulson Even more material from the HOL Light metric space library
23 months ago paulson Importation of additional lemmas from metric.ml
2023-02-07 paulson More new theorems from the number theory development
2023-01-26 paulson Moved in some material from the AFP entry Winding_number_eval
2022-12-21 paulson Additional new material about infinite products, etc.
2021-10-15 paulson A few new lemmas plus some refinements
2021-10-06 eberlm new notion of infinite sums in HOL-Analysis, ordering on complex numbers
2021-06-28 paulson A few useful lemmas about derivatives, colinearity and other topics
2021-06-03 paulson new lemmas mostly about paths
2020-09-08 paulson tidying and de-applying
2020-08-27 paulson but not the [cong] rule
2020-08-27 paulson tidying up some theorem statements
2020-05-13 Manuel Eberl new constant power_int in HOL
2020-05-11 paulson the Uniq quantifier
2019-11-26 paulson Rearrangement of material in Complex_Analysis_Basics, which contained much that had nothing to do with complex analysis.
2019-11-02 paulson Inverse function theorem + lemmas
2019-10-09 haftmann dedicated fact collections for algebraic simplification rules potentially splitting goals
2019-10-09 paulson More theorems about limits, including cancellation simprules
2019-10-09 paulson Generalised two results concerning limits from the real numbers to type classes
2019-09-18 paulson imported new material mostly due to Sébastien Gouëzel
2019-09-13 paulson New theory Equivalence_Measurable_On_Borel, with the HOL Light notion of measurable_on and its equivalence to ours
2019-09-12 paulson new material on Analysis, plus some rearrangements
2019-08-15 paulson new material; rotated premises of Lim_transform_eventually
2019-07-17 paulson a few new lemmas and a bit of tidying
2019-03-18 paulson new material;' strengthened material; moved proofs out of Function_Topology in order to lessen its dependencies
2019-01-04 wenzelm isabelle update -u control_cartouches;
2018-11-08 wenzelm isabelle update_cartouches -t;
2018-09-24 nipkow Prefix form of infix with * on either side no longer needs special treatment
2018-08-30 Manuel Eberl Some basic materials on filters and topology
2018-08-03 eberlm Small lemmas about analysis
2018-07-11 paulson de-applying
2018-07-11 paulson more de-applying
2018-07-10 paulson de-applying, etc.
2018-07-05 paulson de-applying
2018-06-28 paulson Incorporating new/strengthened proofs from Library and AFP entries
2018-05-26 paulson tidying and reorganisation around Cauchy Integral Theorem
2018-05-02 paulson type class generalisations; some work on infinite products
2018-03-28 huffman tuned proofs and generalized some lemmas about limits
2018-03-26 Manuel Eberl Added some simple facts about limits
2018-02-23 Wenda Li merged
2018-02-23 Wenda Li Unified the order of zeros and poles; improved reasoning around non-essential singularites
2018-02-22 immler moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
2018-02-19 paulson lots of new material, ultimately related to measure theory
2018-01-10 nipkow ran isabelle update_op on all sources
2018-01-08 paulson moved in some material from Euler-MacLaurin
2017-11-26 wenzelm more symbols;
2017-10-10 paulson Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems
2017-10-09 paulson new material about connectedness, etc.
2017-08-20 Manuel Eberl Various lemmas for HOL-Analysis
2017-08-17 eberlm Replaced subseq with strict_mono
2017-05-02 paulson Simplification of some proofs. Also key lemmas using !! rather than ! in premises
2017-04-25 paulson New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
2017-03-10 immler modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
2017-02-21 paulson Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion
2016-10-25 paulson more new material
2016-10-18 paulson more from moretop.ml
2016-10-17 nipkow setprod -> prod
2016-10-17 nipkow setsum -> sum
2016-09-28 paulson new material connected with HOL Light measure theory, plus more rationalisation
2016-09-18 wenzelm tuned proofs;
less more (0) -100 -60 tip