| 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
|
| Fri, 07 Mar 2014 15:52:56 +0000 |
paulson |
Some new proofs. Tidying up, esp to remove "apply rule".
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 23:42:43 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
prefer box over greaterThanLessThan on euclidean_space
|
file |
diff |
annotate
|
| Fri, 01 Nov 2013 18:51:14 +0100 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
| Mon, 23 Sep 2013 13:34:15 +0200 |
wenzelm |
proper text for document preparation;
|
file |
diff |
annotate
|
| Sat, 21 Sep 2013 22:33:42 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Thu, 12 Sep 2013 18:09:17 -0700 |
huffman |
make 'linear' into a sublocale of 'bounded_linear';
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 01:12:40 +0200 |
wenzelm |
tuned proofs -- clarified flow of facts wrt. calculation;
|
file |
diff |
annotate
|
| Sun, 18 Aug 2013 19:59:19 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Mon, 22 Apr 2013 18:39:12 +0200 |
immler |
removed type constraints
|
file |
diff |
annotate
|
| Tue, 09 Apr 2013 14:04:47 +0200 |
hoelzl |
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
|
file |
diff |
annotate
|
| Tue, 09 Apr 2013 14:04:41 +0200 |
hoelzl |
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
|
file |
diff |
annotate
|
| Wed, 06 Mar 2013 16:56:21 +0100 |
hoelzl |
changed has_derivative_intros into a named theorems collection
|
file |
diff |
annotate
|
| Thu, 17 Jan 2013 12:21:24 +0100 |
hoelzl |
replace convergent_imp_cauchy by LIMSEQ_imp_Cauchy
|
file |
diff |
annotate
|
| Fri, 14 Dec 2012 15:46:01 +0100 |
hoelzl |
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
|
file |
diff |
annotate
|
| Fri, 07 Dec 2012 14:29:08 +0100 |
hoelzl |
fundamental theorem of calculus for the Lebesgue integral
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 13:31:26 +0100 |
wenzelm |
tuned proofs -- eliminated pointless chaining of facts after 'interpret';
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 21:05:23 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| Tue, 20 Sep 2011 10:52:08 -0700 |
huffman |
add lemmas within_empty and tendsto_bot;
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 11:54:20 -0700 |
huffman |
remove redundant lemma Lim_sequentially in favor of lemma LIMSEQ_def
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Thu, 01 Sep 2011 09:02:14 -0700 |
huffman |
modernize lemmas about 'continuous' and 'continuous_on';
|
file |
diff |
annotate
|
| Sun, 28 Aug 2011 09:20:12 -0700 |
huffman |
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 19:41:38 -0700 |
huffman |
replace some continuous_on lemmas with more general versions
|
file |
diff |
annotate
|
| Tue, 23 Aug 2011 14:11:02 -0700 |
huffman |
declare euclidean_simps [simp] at the point they are proved;
|
file |
diff |
annotate
|
| Thu, 18 Aug 2011 13:36:58 -0700 |
huffman |
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 16:35:50 -0700 |
huffman |
remove several redundant and unused theorems about derivatives
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 14:10:52 -0700 |
huffman |
simplify some proofs
|
file |
diff |
annotate
|
| Tue, 09 Aug 2011 10:30:00 -0700 |
huffman |
mark some redundant theorems as legacy
|
file |
diff |
annotate
|
| Tue, 09 Aug 2011 08:53:12 -0700 |
huffman |
Derivative.thy: more sensible subsection headings
|
file |
diff |
annotate
|
| Tue, 09 Aug 2011 07:37:18 -0700 |
huffman |
Derivative.thy: clean up formatting
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 19:26:53 -0700 |
huffman |
rename type 'a net to 'a filter, following standard mathematical terminology
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 11:50:16 +0200 |
hoelzl |
lemmas about right derivative and limits
|
file |
diff |
annotate
|
| Mon, 14 Mar 2011 14:37:35 +0100 |
hoelzl |
generalize infinite sums
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 22:24:10 +0100 |
wenzelm |
eliminated hard tabs;
|
file |
diff |
annotate
|
| Tue, 22 Feb 2011 16:07:23 +0100 |
hoelzl |
add name continuous_isCont to unnamed lemma
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 10:34:33 +0100 |
hoelzl |
Replace surj by abbreviation; remove surj_on.
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| Sun, 04 Jul 2010 09:26:30 -0700 |
huffman |
generalize some lemmas about derivatives
|
file |
diff |
annotate
|