| 2021-07-08 |
desharna |
merged
|
file |
diff |
annotate
|
| 2021-07-08 |
desharna |
added opaque_combs and renamed hide_lams to opaque_lifting
|
file |
diff |
annotate
|
| 2021-06-30 |
paulson |
just a bit of tidying up
|
file |
diff |
annotate
|
| 2020-12-25 |
paulson |
A few more simprules for iff-reasoning
|
file |
diff |
annotate
|
| 2020-12-24 |
paulson |
Two biconditional simprules for summable
|
file |
diff |
annotate
|
| 2020-12-23 |
paulson |
default simprule for geometric series
|
file |
diff |
annotate
|
| 2020-08-27 |
paulson |
tidying up some theorem statements
|
file |
diff |
annotate
|
| 2020-05-11 |
paulson |
the Uniq quantifier
|
file |
diff |
annotate
|
| 2019-09-18 |
paulson |
imported new material mostly due to Sébastien Gouëzel
|
file |
diff |
annotate
|
| 2019-04-10 |
paulson |
Fixing the main Homology theory; also moving a lot of sum/prod lemmas into their generic context
|
file |
diff |
annotate
|
| 2019-04-10 |
paulson |
The last big tranche of Homology material: invariance of domain; renamings to use generic sum/prod lemmas from their locale
|
file |
diff |
annotate
|
| 2019-01-04 |
wenzelm |
isabelle update -u control_cartouches;
|
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-05 |
paulson |
de-applying
|
file |
diff |
annotate
|
| 2018-06-28 |
paulson |
Generalising and renaming some basic results
|
file |
diff |
annotate
|
| 2018-06-26 |
paulson |
Rationalisation of complex transcendentals, esp the Arg function
|
file |
diff |
annotate
|
| 2018-05-09 |
paulson |
more infinite product theorems
|
file |
diff |
annotate
|
| 2018-05-02 |
paulson |
type class generalisations; some work on infinite products
|
file |
diff |
annotate
|
| 2017-12-22 |
paulson |
new/improved theories involving convergence; better pretty-printing for bounded quantifiers and sum/product
|
file |
diff |
annotate
|
| 2017-12-12 |
Manuel Eberl |
Moved analysis material from AFP
|
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
|
| 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-08-12 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| 2016-07-26 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| 2016-07-02 |
haftmann |
more theorems
|
file |
diff |
annotate
|
| 2016-05-25 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| 2016-04-25 |
wenzelm |
eliminated old 'def';
|
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-12 |
hoelzl |
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
|
file |
diff |
annotate
|
| 2016-02-10 |
hoelzl |
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
|
file |
diff |
annotate
|
| 2016-02-08 |
hoelzl |
add type class for topological monoids
|
file |
diff |
annotate
|
| 2016-01-22 |
paulson |
Reorganised a huge proof
|
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-29 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| 2015-12-07 |
wenzelm |
isabelle update_cartouches -c -t;
|
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 |
Rounding function, uniform limits, cotangent, binomial identities
|
file |
diff |
annotate
|
| 2015-08-06 |
haftmann |
slight cleanup of lemmas
|
file |
diff |
annotate
|
| 2015-07-18 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| 2015-04-21 |
paulson |
New material, mostly about limits. Consolidation.
|
file |
diff |
annotate
|
| 2015-03-18 |
paulson |
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
|
file |
diff |
annotate
|
| 2015-03-16 |
hoelzl |
add inequalities (move from AFP/Amortized_Complexity)
|
file |
diff |
annotate
|
| 2015-03-05 |
paulson |
The function frac. Various lemmas about limits, series, the exp function, etc.
|
file |
diff |
annotate
|
| 2014-11-21 |
Andreas Lochbihler |
add lemma following a proof suggestion by Joachim Breitner
|
file |
diff |
annotate
|
| 2014-11-13 |
hoelzl |
import general theorems from AFP/Markov_Models
|
file |
diff |
annotate
|
| 2014-11-02 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| 2014-10-20 |
hoelzl |
add tendsto_const and tendsto_ident_at as simp and intro rules
|
file |
diff |
annotate
|
| 2014-06-28 |
haftmann |
fact consolidation
|
file |
diff |
annotate
|
| 2014-06-18 |
hoelzl |
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
|
file |
diff |
annotate
|
| 2014-05-30 |
hoelzl |
introduce more powerful reindexing rules for big operators
|
file |
diff |
annotate
|
| 2014-05-20 |
hoelzl |
add various lemmas
|
file |
diff |
annotate
|
| 2014-04-11 |
nipkow |
made mult_nonneg_nonneg a simp rule
|
file |
diff |
annotate
|
| 2014-04-02 |
hoelzl |
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
|
file |
diff |
annotate
|
| 2014-03-19 |
paulson |
Some rationalisation of basic lemmas
|
file |
diff |
annotate
|