Wed, 13 Jul 2016 17:14:17 +0100 |
paulson |
lots of new theorems about differentiable_on, retracts, ANRs, etc.
|
file |
diff |
annotate
|
Fri, 27 May 2016 20:23:55 +0200 |
wenzelm |
tuned proofs, to allow unfold_abs_def;
|
file |
diff |
annotate
|
Tue, 24 May 2016 13:57:34 +0100 |
paulson |
renamings and new material
|
file |
diff |
annotate
|
Tue, 10 May 2016 15:48:37 +0200 |
immler |
some slight generalizations
|
file |
diff |
annotate
|
Mon, 25 Apr 2016 16:09:26 +0200 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
Tue, 12 Apr 2016 11:18:29 +0200 |
immler |
added derivative of scaling in exponential function
|
file |
diff |
annotate
|
Mon, 07 Mar 2016 14:34:45 +0000 |
paulson |
new material to Blochj's theorem, as well as supporting lemmas
|
file |
diff |
annotate
|
Thu, 25 Feb 2016 13:58:48 +0000 |
paulson |
Conformal_mappings: a big development in complex analysis (+ some lemmas)
|
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
|
Wed, 20 Jan 2016 13:16:58 +0100 |
immler |
added lemma
|
file |
diff |
annotate
|
Fri, 08 Jan 2016 17:40:59 +0100 |
hoelzl |
add uniform spaces
|
file |
diff |
annotate
|
Thu, 07 Jan 2016 17:40:55 +0000 |
paulson |
revisions to limits and derivatives, plus new lemmas
|
file |
diff |
annotate
|
Wed, 30 Dec 2015 11:37:29 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
Wed, 30 Dec 2015 11:21:54 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
Tue, 29 Dec 2015 23:04:53 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
Mon, 28 Dec 2015 01:28:28 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
Tue, 22 Dec 2015 21:58:27 +0100 |
immler |
theory for type of bounded linear functions; differentiation under the integral sign
|
file |
diff |
annotate
|
Tue, 22 Dec 2015 14:33:34 +0000 |
paulson |
Liouville theorem, Fundamental Theorem of Algebra, etc.
|
file |
diff |
annotate
|
Thu, 17 Dec 2015 16:43:36 +0100 |
hoelzl |
moved some theorems from the CLT proof; reordered some theorems / notation
|
file |
diff |
annotate
|
Thu, 10 Dec 2015 13:38:40 +0000 |
paulson |
not_leE -> not_le_imp_less and other tidying
|
file |
diff |
annotate
|
Wed, 09 Dec 2015 17:35:22 +0000 |
paulson |
sorted out eventually_mono
|
file |
diff |
annotate
|
Mon, 07 Dec 2015 20:19:59 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
Tue, 01 Dec 2015 14:09:10 +0000 |
paulson |
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
|
file |
diff |
annotate
|
Fri, 13 Nov 2015 12:27:13 +0000 |
paulson |
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
|
file |
diff |
annotate
|
Tue, 03 Nov 2015 16:47:37 +0100 |
wenzelm |
tuned imports;
|
file |
diff |
annotate
|
Mon, 02 Nov 2015 11:56:28 +0100 |
eberlm |
Rounding function, uniform limits, cotangent, binomial identities
|
file |
diff |
annotate
|
Thu, 29 Oct 2015 15:40:52 +0100 |
eberlm |
added many small lemmas about setsum/setprod/powr/...
|
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
|
Mon, 26 Oct 2015 23:41:27 +0000 |
paulson |
new lemmas about topology, etc., for Cauchy integral formula
|
file |
diff |
annotate
|
Fri, 25 Sep 2015 16:54:31 +0200 |
hoelzl |
prove Liminf_inverse_ereal
|
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 16:50:12 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Thu, 03 Sep 2015 20:27:53 +0100 |
paulson |
new lemmas about vector_derivative, complex numbers, paths, etc.
|
file |
diff |
annotate
|
Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
Mon, 27 Jul 2015 16:52:57 +0100 |
paulson |
New material for Cauchy's integral theorem
|
file |
diff |
annotate
|
Mon, 20 Jul 2015 23:12:50 +0100 |
paulson |
new material for multivariate analysis, etc.
|
file |
diff |
annotate
|
Fri, 26 Jun 2015 14:53:28 +0200 |
wenzelm |
do not expose goal parameters;
|
file |
diff |
annotate
|
Wed, 10 Jun 2015 19:10:20 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
Tue, 05 May 2015 18:45:10 +0200 |
immler |
generalized class constraints
|
file |
diff |
annotate
|
Tue, 05 May 2015 18:45:10 +0200 |
immler |
generalized differentiable_bound; some further variations of differentiable_bound
|
file |
diff |
annotate
|
Tue, 05 May 2015 18:45:10 +0200 |
immler |
moved basic lemmas about has_vector_derivative
|
file |
diff |
annotate
|
Mon, 23 Mar 2015 19:05:14 +0100 |
haftmann |
explicit commutative additive inverse operation;
|
file |
diff |
annotate
|
Thu, 19 Feb 2015 17:01:46 +0000 |
paulson |
got rid of linordered_field_class.sign_simps(41) !
|
file |
diff |
annotate
|
Sun, 02 Nov 2014 17:09:04 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
Tue, 05 Aug 2014 16:58:19 +0200 |
wenzelm |
tuned proofs -- fewer warnings;
|
file |
diff |
annotate
|
Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
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
|
Mon, 16 Jun 2014 17:52:33 +0200 |
hoelzl |
add more derivative and continuity rules for complex-values functions
|
file |
diff |
annotate
|
Fri, 11 Apr 2014 22:53:33 +0200 |
nipkow |
made divide_pos_pos a simp rule
|
file |
diff |
annotate
|
Sun, 06 Apr 2014 21:01:33 +0200 |
nipkow |
tuned lemmas: more general class
|
file |
diff |
annotate
|
Thu, 03 Apr 2014 17:56:08 +0200 |
hoelzl |
merged DERIV_intros, has_derivative_intros into derivative_intros
|
file |
diff |
annotate
|
Wed, 02 Apr 2014 18:35:07 +0200 |
hoelzl |
extend continuous_intros; remove continuous_on_intros and isCont_intros
|
file |
diff |
annotate
|
Wed, 02 Apr 2014 18:35:02 +0200 |
hoelzl |
reorder Complex_Analysis_Basics; rename DD to deriv
|
file |
diff |
annotate
|
Wed, 02 Apr 2014 18:35:01 +0200 |
hoelzl |
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
|
file |
diff |
annotate
|
Mon, 31 Mar 2014 17:17:37 +0200 |
hoelzl |
tuned proofs
|
file |
diff |
annotate
|
Fri, 28 Mar 2014 18:21:07 -0700 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
Mon, 24 Mar 2014 14:51:10 -0700 |
huffman |
generalized theorems about derivatives of limits of sequences of funtions
|
file |
diff |
annotate
|
Thu, 20 Mar 2014 17:55:33 -0700 |
huffman |
tuned proofs
|
file |
diff |
annotate
|