| 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
|
| Mon, 24 Mar 2014 14:22:29 +0000 |
paulson |
rearranging some deriv theorems
|
file |
diff |
annotate
|
| Thu, 20 Mar 2014 15:13:55 -0700 |
huffman |
generalize more theorems
|
file |
diff |
annotate
|
| Thu, 20 Mar 2014 09:21:39 -0700 |
huffman |
generalize some theorems
|
file |
diff |
annotate
|
| Wed, 19 Mar 2014 20:50:24 -0700 |
huffman |
generalize theory of operator norms to work with class real_normed_vector
|
file |
diff |
annotate
|
| Wed, 19 Mar 2014 17:06:02 +0000 |
paulson |
Some rationalisation of basic lemmas
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 09:39:07 -0700 |
huffman |
remove unnecessary finiteness assumptions from lemmas about setsum
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 15:53:48 +0100 |
hoelzl |
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 10:12:57 +0100 |
immler |
use cbox to relax class constraints
|
file |
diff |
annotate
|
| Mon, 17 Mar 2014 20:38:50 +0100 |
hoelzl |
remove sums_seq, it is not used
|
file |
diff |
annotate
|
| Mon, 17 Mar 2014 19:50:59 +0100 |
hoelzl |
update syntax of has_*derivative to infix 50; fixed proofs
|
file |
diff |
annotate
|
| Mon, 17 Mar 2014 19:12:52 +0100 |
hoelzl |
unify syntax for has_derivative and differentiable
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 13:27:38 -0700 |
huffman |
add lemmas about nhds filter; tuned proof
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 10:59:43 -0700 |
huffman |
remove unused lemma which was a direct consequence of tendsto_intros
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 09:09:33 -0700 |
huffman |
generalization of differential_zero_maxmin to class real_normed_vector
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 16:07:27 -0700 |
huffman |
remove ordered_euclidean_space constraint from brouwer/derivative lemmas;
|
file |
diff |
annotate
|