| 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
|
| Wed, 11 May 2016 16:13:17 +0200 |
immler |
introduced class topological_group between topological_monoid and real_normed_vector
|
file |
diff |
annotate
|
| Mon, 25 Apr 2016 16:09:26 +0200 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 18:04:31 +0100 |
nipkow |
resolved conflict
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 15:47:39 +0000 |
paulson |
New and revised material for (multivariate) analysis
|
file |
diff |
annotate
|
| Mon, 22 Feb 2016 14:37:56 +0000 |
paulson |
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
|
file |
diff |
annotate
|
| Tue, 09 Feb 2016 06:39:31 +0100 |
hoelzl |
instantiate topologies for nat, int and enat
|
file |
diff |
annotate
|