| Fri, 23 Jun 2017 13:16:04 +0200 |
eberlm |
distrib_lattice instance for filters
|
file |
diff |
annotate
|
| Thu, 22 Jun 2017 10:50:18 +0200 |
eberlm |
Contravariant map on filters
|
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, 30 Sep 2016 14:05:51 +0100 |
paulson |
new material on paths, etc. Also rationalisation
|
file |
diff |
annotate
|
| Thu, 28 Jul 2016 17:16:16 +0200 |
immler |
numerical bounds on pi
|
file |
diff |
annotate
|
| Fri, 22 Jul 2016 11:00:43 +0200 |
wenzelm |
tuned proofs -- avoid unstructured calculation;
|
file |
diff |
annotate
|
| Wed, 22 Jun 2016 10:09:20 +0200 |
wenzelm |
bundle lifting_syntax;
|
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
|
| Fri, 19 Feb 2016 13:40:50 +0100 |
hoelzl |
generalize more theorems to support enat and ennreal
|
file |
diff |
annotate
|
| Tue, 09 Feb 2016 06:39:31 +0100 |
hoelzl |
instantiate topologies for nat, int and enat
|
file |
diff |
annotate
|
| Mon, 08 Feb 2016 17:18:13 +0100 |
hoelzl |
move product topology to HOL-Complex_Main
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:56 +0100 |
haftmann |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
file |
diff |
annotate
|
| Mon, 11 Jan 2016 11:56:35 +0100 |
hoelzl |
setup code generation for filters as suggested by Florian
|
file |
diff |
annotate
|
| Fri, 08 Jan 2016 17:41:04 +0100 |
hoelzl |
fix code generation for uniformity: uniformity is a non-computable pure data.
|
file |
diff |
annotate
|
| Fri, 08 Jan 2016 17:40:59 +0100 |
hoelzl |
add uniform spaces
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 21:47:32 +0100 |
wenzelm |
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 18:03:26 +0100 |
wenzelm |
use symbols by default;
|
file |
diff |
annotate
|
| Sun, 13 Dec 2015 21:56:15 +0100 |
wenzelm |
more general types Proof.method / context_tactic;
|
file |
diff |
annotate
|
| Wed, 09 Dec 2015 17:35:22 +0000 |
paulson |
sorted out eventually_mono
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 16:44:26 +0000 |
paulson |
Cauchy's integral formula for circles. Starting to fix eventually_mono.
|
file |
diff |
annotate
|
| Mon, 02 Nov 2015 11:56:28 +0100 |
eberlm |
Rounding function, uniform limits, cotangent, binomial identities
|
file |
diff |
annotate
|
| Fri, 09 Oct 2015 20:26:03 +0200 |
wenzelm |
discontinued specific HTML syntax;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 16:54:31 +0200 |
hoelzl |
prove Liminf_inverse_ereal
|
file |
diff |
annotate
|
| Tue, 22 Sep 2015 16:53:59 +0100 |
paulson |
Prepared two non-terminating proofs; no obvious link with my changes
|
file |
diff |
annotate
|
| Wed, 19 Aug 2015 19:18:19 +0100 |
paulson |
New material and fixes related to the forthcoming Stone-Weierstrass development
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 20:47:08 +0200 |
wenzelm |
prefer tactics with explicit context;
|
file |
diff |
annotate
|
| Tue, 14 Jul 2015 13:48:03 +0200 |
hoelzl |
generalized filtermap_homeomorph to filtermap_fun_inverse; add eventually_at_top/bot_not_equal
|
file |
diff |
annotate
|
| Fri, 26 Jun 2015 14:53:28 +0200 |
wenzelm |
do not expose goal parameters;
|
file |
diff |
annotate
|
| Thu, 07 May 2015 15:34:28 +0200 |
hoelzl |
generalized tends over powr; added DERIV rule for powr
|
file |
diff |
annotate
|
| Sun, 12 Apr 2015 11:34:09 +0200 |
hoelzl |
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
|
file |
diff |
annotate
|
| Sun, 12 Apr 2015 11:33:50 +0200 |
hoelzl |
add cofinite filter
|
file |
diff |
annotate
|
| Sun, 12 Apr 2015 11:33:44 +0200 |
hoelzl |
add frequently as dual for eventually
|
file |
diff |
annotate
|
| Sun, 12 Apr 2015 11:33:30 +0200 |
hoelzl |
add quantifier syntax for eventually
|
file |
diff |
annotate
|
| Sun, 12 Apr 2015 11:33:19 +0200 |
hoelzl |
move filters to their own theory
|
file |
diff |
annotate
|