| Mon, 02 Nov 2015 11:56:28 +0100 |
eberlm |
Rounding function, uniform limits, cotangent, binomial identities
|
file |
diff |
annotate
|
| Tue, 27 Oct 2015 15:17:02 +0000 |
paulson |
Cauchy's integral formula, required lemmas, and a bit of reorganisation
|
file |
diff |
annotate
|
| Tue, 13 Oct 2015 12:42:08 +0100 |
paulson |
new material on path_component_sets, inside, outside, etc. And more default simprules
|
file |
diff |
annotate
|
| Tue, 06 Oct 2015 17:46:07 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Fri, 02 Oct 2015 15:07:41 +0100 |
paulson |
New theorems about connected sets. And pairwise moved to Set.thy.
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 16:54:31 +0200 |
hoelzl |
prove Liminf_inverse_ereal
|
file |
diff |
annotate
|
| Tue, 22 Sep 2015 16:55:07 +0100 |
paulson |
New lemmas
|
file |
diff |
annotate
|
| Mon, 21 Sep 2015 19:52:13 +0100 |
paulson |
new lemmas and movement of lemmas into place
|
file |
diff |
annotate
|
| Sun, 13 Sep 2015 22:56:52 +0200 |
wenzelm |
tuned proofs -- less legacy;
|
file |
diff |
annotate
|
| Mon, 20 Jul 2015 23:12:50 +0100 |
paulson |
new material for multivariate analysis, etc.
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Tue, 14 Jul 2015 13:37:44 +0200 |
hoelzl |
add continuous_onI_mono
|
file |
diff |
annotate
|
| Fri, 26 Jun 2015 10:20:33 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Thu, 07 May 2015 15:34:28 +0200 |
hoelzl |
generalized tends over powr; added DERIV rule for powr
|
file |
diff |
annotate
|
| Mon, 04 May 2015 17:35:31 +0200 |
hoelzl |
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
|
file |
diff |
annotate
|
| Tue, 28 Apr 2015 16:23:38 +0100 |
paulson |
New material about complex transcendental functions (especially Ln, Arg) and polynomials
|
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:19 +0200 |
hoelzl |
move filters to their own theory
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 21:42:08 +0200 |
wenzelm |
more standard access to goal state;
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 19:58:52 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 19:39:08 +0200 |
wenzelm |
proper context for Object_Logic operations;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Tue, 27 Jan 2015 16:12:40 +0100 |
hoelzl |
ereal: tuned proofs concerning continuity and suprema
|
file |
diff |
annotate
|
| Mon, 08 Dec 2014 14:32:11 +0100 |
hoelzl |
instance bool and enat as topologies
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Mon, 20 Oct 2014 18:33:14 +0200 |
hoelzl |
add tendsto_const and tendsto_ident_at as simp and intro rules
|
file |
diff |
annotate
|
| Sat, 16 Aug 2014 14:42:35 +0200 |
wenzelm |
updated to named_theorems;
|
file |
diff |
annotate
|
| Mon, 30 Jun 2014 15:45:25 +0200 |
hoelzl |
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
|
file |
diff |
annotate
|
| Mon, 30 Jun 2014 15:45:21 +0200 |
hoelzl |
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
|
file |
diff |
annotate
|
| Wed, 18 Jun 2014 14:31:32 +0200 |
hoelzl |
filters are easier to define with INF on filters.
|
file |
diff |
annotate
|