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