| 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
|
| 2016-08-25 |
Manuel Eberl |
More analysis lemmas
|
file |
diff |
annotate
|
| 2016-07-28 |
immler |
numerical bounds on pi
|
file |
diff |
annotate
|
| 2016-07-25 |
wenzelm |
unused (see 1e9e68247ad1);
|
file |
diff |
annotate
|
| 2016-07-22 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| 2016-06-14 |
paulson |
new results about topology
|
file |
diff |
annotate
|
| 2016-06-09 |
immler |
approximation, derivative, and continuity of floor and ceiling
|
file |
diff |
annotate
|
| 2016-05-20 |
immler |
reduce isUCont to uniformly_continuous_on
|
file |
diff |
annotate
|
| 2016-05-11 |
immler |
introduced class topological_group between topological_monoid and real_normed_vector
|
file |
diff |
annotate
|
| 2016-04-25 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
| 2016-02-23 |
nipkow |
resolved conflict
|
file |
diff |
annotate
|
| 2016-02-23 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| 2016-02-23 |
paulson |
New and revised material for (multivariate) analysis
|
file |
diff |
annotate
|
| 2016-02-22 |
paulson |
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
|
file |
diff |
annotate
|
| 2016-02-09 |
hoelzl |
instantiate topologies for nat, int and enat
|
file |
diff |
annotate
|
| 2016-02-08 |
hoelzl |
add type class for topological monoids
|
file |
diff |
annotate
|
| 2016-01-08 |
hoelzl |
add uniform spaces
|
file |
diff |
annotate
|
| 2016-01-07 |
paulson |
revisions to limits and derivatives, plus new lemmas
|
file |
diff |
annotate
|
| 2015-12-30 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| 2015-12-30 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| 2015-12-29 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| 2015-12-23 |
immler |
transfer rule for bounded_linear of blinfun
|
file |
diff |
annotate
|
| 2015-12-09 |
paulson |
sorted out eventually_mono
|
file |
diff |
annotate
|
| 2015-12-07 |
paulson |
Cauchy's integral formula for circles. Starting to fix eventually_mono.
|
file |
diff |
annotate
|
| 2015-12-07 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| 2015-11-23 |
paulson |
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
|
file |
diff |
annotate
|
| 2015-11-17 |
paulson |
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
|
file |
diff |
annotate
|
| 2015-11-13 |
paulson |
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
|
file |
diff |
annotate
|
| 2015-11-10 |
paulson |
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
|
file |
diff |
annotate
|
| 2015-11-02 |
eberlm |
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
|
file |
diff |
annotate
|
| 2015-11-02 |
eberlm |
Rounding function, uniform limits, cotangent, binomial identities
|
file |
diff |
annotate
|