| Mon, 28 Jun 2021 15:05:46 +0100 |
paulson |
A few useful lemmas about derivatives, colinearity and other topics
|
file |
diff |
annotate
|
| Thu, 03 Jun 2021 10:47:20 +0100 |
paulson |
new lemmas mostly about paths
|
file |
diff |
annotate
|
| Tue, 08 Sep 2020 15:30:15 +0100 |
paulson |
tidying and de-applying
|
file |
diff |
annotate
|
| Thu, 27 Aug 2020 15:23:48 +0100 |
paulson |
but not the [cong] rule
|
file |
diff |
annotate
|
| Thu, 27 Aug 2020 12:14:46 +0100 |
paulson |
tidying up some theorem statements
|
file |
diff |
annotate
|
| Wed, 13 May 2020 12:55:33 +0200 |
Manuel Eberl |
new constant power_int in HOL
|
file |
diff |
annotate
|
| Mon, 11 May 2020 11:15:41 +0100 |
paulson |
the Uniq quantifier
|
file |
diff |
annotate
|
| Tue, 26 Nov 2019 14:32:08 +0000 |
paulson |
Rearrangement of material in Complex_Analysis_Basics, which contained much that had nothing to do with complex analysis.
|
file |
diff |
annotate
|
| Sat, 02 Nov 2019 14:31:34 +0000 |
paulson |
Inverse function theorem + lemmas
|
file |
diff |
annotate
|
| Wed, 09 Oct 2019 14:51:54 +0000 |
haftmann |
dedicated fact collections for algebraic simplification rules potentially splitting goals
|
file |
diff |
annotate
|
| Wed, 09 Oct 2019 15:32:41 +0100 |
paulson |
More theorems about limits, including cancellation simprules
|
file |
diff |
annotate
|
| Wed, 09 Oct 2019 14:39:10 +0100 |
paulson |
Generalised two results concerning limits from the real numbers to type classes
|
file |
diff |
annotate
|
| Wed, 18 Sep 2019 14:41:37 +0100 |
paulson |
imported new material mostly due to Sébastien Gouëzel
|
file |
diff |
annotate
|
| Fri, 13 Sep 2019 12:46:36 +0100 |
paulson |
New theory Equivalence_Measurable_On_Borel, with the HOL Light notion of measurable_on and its equivalence to ours
|
file |
diff |
annotate
|
| Thu, 12 Sep 2019 14:51:45 +0100 |
paulson |
new material on Analysis, plus some rearrangements
|
file |
diff |
annotate
|
| Thu, 15 Aug 2019 16:11:56 +0100 |
paulson |
new material; rotated premises of Lim_transform_eventually
|
file |
diff |
annotate
|
| Wed, 17 Jul 2019 14:02:42 +0100 |
paulson |
a few new lemmas and a bit of tidying
|
file |
diff |
annotate
|
| Mon, 18 Mar 2019 15:35:34 +0000 |
paulson |
new material;' strengthened material; moved proofs out of Function_Topology in order to lessen its dependencies
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Thu, 08 Nov 2018 22:29:09 +0100 |
wenzelm |
isabelle update_cartouches -t;
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 14:30:09 +0200 |
nipkow |
Prefix form of infix with * on either side no longer needs special treatment
|
file |
diff |
annotate
|
| Thu, 30 Aug 2018 17:20:54 +0200 |
Manuel Eberl |
Some basic materials on filters and topology
|
file |
diff |
annotate
|
| Sat, 04 Aug 2018 01:03:39 +0200 |
eberlm |
Small lemmas about analysis
|
file |
diff |
annotate
|
| Wed, 11 Jul 2018 19:19:00 +0100 |
paulson |
de-applying
|
file |
diff |
annotate
|
| Wed, 11 Jul 2018 15:36:12 +0100 |
paulson |
more de-applying
|
file |
diff |
annotate
|
| Tue, 10 Jul 2018 23:18:08 +0100 |
paulson |
de-applying, etc.
|
file |
diff |
annotate
|
| Thu, 05 Jul 2018 23:37:00 +0100 |
paulson |
de-applying
|
file |
diff |
annotate
|
| Thu, 28 Jun 2018 17:14:40 +0100 |
paulson |
Incorporating new/strengthened proofs from Library and AFP entries
|
file |
diff |
annotate
|
| Sat, 26 May 2018 22:11:55 +0100 |
paulson |
tidying and reorganisation around Cauchy Integral Theorem
|
file |
diff |
annotate
|
| Wed, 02 May 2018 12:47:56 +0100 |
paulson |
type class generalisations; some work on infinite products
|
file |
diff |
annotate
|
| Wed, 28 Mar 2018 12:13:21 -0700 |
huffman |
tuned proofs and generalized some lemmas about limits
|
file |
diff |
annotate
|
| Mon, 26 Mar 2018 16:12:55 +0200 |
Manuel Eberl |
Added some simple facts about limits
|
file |
diff |
annotate
|
| Fri, 23 Feb 2018 14:56:32 +0000 |
Wenda Li |
merged
|
file |
diff |
annotate
|
| Fri, 23 Feb 2018 13:27:19 +0000 |
Wenda Li |
Unified the order of zeros and poles; improved reasoning around non-essential singularites
|
file |
diff |
annotate
|
| Thu, 22 Feb 2018 15:17:25 +0100 |
immler |
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
|
file |
diff |
annotate
|
| Mon, 19 Feb 2018 16:44:45 +0000 |
paulson |
lots of new material, ultimately related to measure theory
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Mon, 08 Jan 2018 17:11:25 +0000 |
paulson |
moved in some material from Euler-MacLaurin
|
file |
diff |
annotate
|
| Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 10 Oct 2017 17:15:37 +0100 |
paulson |
Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems
|
file |
diff |
annotate
|
| Mon, 09 Oct 2017 15:34:23 +0100 |
paulson |
new material about connectedness, etc.
|
file |
diff |
annotate
|
| Sun, 20 Aug 2017 03:35:20 +0200 |
Manuel Eberl |
Various lemmas for HOL-Analysis
|
file |
diff |
annotate
|
| Thu, 17 Aug 2017 14:52:56 +0200 |
eberlm |
Replaced subseq with strict_mono
|
file |
diff |
annotate
|
| Tue, 02 May 2017 14:34:06 +0100 |
paulson |
Simplification of some proofs. Also key lemmas using !! rather than ! in premises
|
file |
diff |
annotate
|
| Tue, 25 Apr 2017 16:39:54 +0100 |
paulson |
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
|
file |
diff |
annotate
|
| Fri, 10 Mar 2017 23:16:40 +0100 |
immler |
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
|
file |
diff |
annotate
|
| Tue, 21 Feb 2017 15:04:01 +0000 |
paulson |
Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion
|
file |
diff |
annotate
|
| Tue, 25 Oct 2016 15:46:07 +0100 |
paulson |
more new material
|
file |
diff |
annotate
|
| Tue, 18 Oct 2016 15:55:53 +0100 |
paulson |
more from moretop.ml
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 17:33:07 +0200 |
nipkow |
setprod -> prod
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
| Wed, 28 Sep 2016 17:01:01 +0100 |
paulson |
new material connected with HOL Light measure theory, plus more rationalisation
|
file |
diff |
annotate
|
| Sun, 18 Sep 2016 20:33:48 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Thu, 25 Aug 2016 15:50:43 +0200 |
Manuel Eberl |
More analysis lemmas
|
file |
diff |
annotate
|
| Thu, 28 Jul 2016 17:16:16 +0200 |
immler |
numerical bounds on pi
|
file |
diff |
annotate
|
| Mon, 25 Jul 2016 14:02:29 +0200 |
wenzelm |
unused (see 1e9e68247ad1);
|
file |
diff |
annotate
|
| Fri, 22 Jul 2016 23:55:47 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Tue, 14 Jun 2016 15:34:21 +0100 |
paulson |
new results about topology
|
file |
diff |
annotate
|
| Thu, 09 Jun 2016 16:04:20 +0200 |
immler |
approximation, derivative, and continuity of floor and ceiling
|
file |
diff |
annotate
|
| Fri, 20 May 2016 21:21:28 +0200 |
immler |
reduce isUCont to uniformly_continuous_on
|
file |
diff |
annotate
|