| 2019-04-01 |
paulson |
A few results in Algebra, and bits for Analysis
|
file |
diff |
annotate
|
| 2019-01-21 |
paulson |
new material about summations and powers, along with some tweaks
|
file |
diff |
annotate
|
| 2019-01-04 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| 2018-12-27 |
immler |
moved lemmas up
|
file |
diff |
annotate
|
| 2018-12-27 |
immler |
prove lemmas in context real_normed_vector
|
file |
diff |
annotate
|
| 2018-11-08 |
haftmann |
removed relics of ASCII syntax for indexed big operators
|
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-03 |
eberlm |
Small lemmas about analysis
|
file |
diff |
annotate
|
| 2018-07-21 |
paulson |
de-applying and removing junk
|
file |
diff |
annotate
|
| 2018-07-11 |
paulson |
de-applying
|
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-06-26 |
paulson |
Rationalisation of complex transcendentals, esp the Arg function
|
file |
diff |
annotate
|
| 2018-06-18 |
paulson |
New material in support of quaternions
|
file |
diff |
annotate
|
| 2018-06-06 |
wenzelm |
isabelle update_comments;
|
file |
diff |
annotate
|
| 2018-05-02 |
immler |
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
|
file |
diff |
annotate
|
| 2018-02-26 |
immler |
moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements
|
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-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
|
| 2017-12-05 |
Manuel Eberl |
Moved material from AFP to Analysis/Number_Theory
|
file |
diff |
annotate
|
| 2017-10-09 |
paulson |
new material about connectedness, etc.
|
file |
diff |
annotate
|
| 2017-08-14 |
paulson |
patching the previous commit
|
file |
diff |
annotate
|
| 2017-08-14 |
paulson |
further Hensock tidy-up
|
file |
diff |
annotate
|
| 2017-06-15 |
paulson |
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
|
file |
diff |
annotate
|
| 2017-05-02 |
paulson |
Simplification of some proofs. Also key lemmas using !! rather than ! in premises
|
file |
diff |
annotate
|
| 2017-04-26 |
paulson |
Further new material. The simprule status of some exp and ln identities was reverted.
|
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-02-21 |
paulson |
Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion
|
file |
diff |
annotate
|
| 2017-01-05 |
paulson |
New material about path connectedness, etc.
|
file |
diff |
annotate
|
| 2016-10-17 |
nipkow |
setprod -> prod
|
file |
diff |
annotate
|
| 2016-10-17 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
| 2016-10-16 |
haftmann |
more standardized names
|
file |
diff |
annotate
|
| 2016-09-30 |
paulson |
new material on paths, etc. Also rationalisation
|
file |
diff |
annotate
|
| 2016-09-21 |
paulson |
vector_add_divide_simps now a "named theorems" bundle
|
file |
diff |
annotate
|
| 2016-09-18 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| 2016-08-12 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| 2016-07-28 |
immler |
numerical bounds on pi
|
file |
diff |
annotate
|
| 2016-07-22 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| 2016-07-13 |
paulson |
lots of new theorems about differentiable_on, retracts, ANRs, etc.
|
file |
diff |
annotate
|
| 2016-05-24 |
paulson |
renamings and new material
|
file |
diff |
annotate
|
| 2016-05-23 |
paulson |
Lots of new material for multivariate analysis
|
file |
diff |
annotate
|
| 2016-04-25 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
| 2016-04-11 |
paulson |
lots of new theorems for multivariate analysis
|
file |
diff |
annotate
|
| 2016-03-15 |
paulson |
rationalisation of theorem names esp about "real Archimedian" etc.
|
file |
diff |
annotate
|
| 2016-03-07 |
paulson |
new material to Blochj's theorem, as well as supporting lemmas
|
file |
diff |
annotate
|
| 2016-02-24 |
paulson |
Substantial new material for multivariate analysis. Also removal of some duplicates.
|
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-08 |
hoelzl |
add type class for topological monoids
|
file |
diff |
annotate
|
| 2016-02-17 |
haftmann |
generalized some lemmas;
|
file |
diff |
annotate
|
| 2016-01-11 |
paulson |
nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
|
file |
diff |
annotate
|
| 2016-01-08 |
hoelzl |
fix code generation for uniformity: uniformity is a non-computable pure data.
|
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
|
| 2016-01-04 |
eberlm |
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
|
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-27 |
wenzelm |
prefer symbols for "floor", "ceiling";
|
file |
diff |
annotate
|
| 2015-12-23 |
immler |
transfer rule for bounded_linear of blinfun
|
file |
diff |
annotate
|