| Thu, 17 Jan 2013 12:21:24 +0100 |
replace convergent_imp_cauchy by LIMSEQ_imp_Cauchy
|
file | diff | annotate |
| Fri, 14 Dec 2012 15:46:01 +0100 |
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 |
fundamental theorem of calculus for the Lebesgue integral
|
file | diff | annotate |
| Tue, 13 Mar 2012 13:31:26 +0100 |
tuned proofs -- eliminated pointless chaining of facts after 'interpret';
|
file | diff | annotate |
| Sun, 20 Nov 2011 21:05:23 +0100 |
eliminated obsolete "standard";
|
file | diff | annotate |
| Tue, 20 Sep 2011 10:52:08 -0700 |
add lemmas within_empty and tendsto_bot;
|
file | diff | annotate |
| Mon, 12 Sep 2011 11:54:20 -0700 |
remove redundant lemma Lim_sequentially in favor of lemma LIMSEQ_def
|
file | diff | annotate |
| Mon, 12 Sep 2011 07:55:43 +0200 |
new fastforce replacing fastsimp - less confusing name
|
file | diff | annotate |
| Thu, 01 Sep 2011 09:02:14 -0700 |
modernize lemmas about 'continuous' and 'continuous_on';
|
file | diff | annotate |
| Sun, 28 Aug 2011 09:20:12 -0700 |
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
|
file | diff | annotate |
| Thu, 25 Aug 2011 19:41:38 -0700 |
replace some continuous_on lemmas with more general versions
|
file | diff | annotate |
| Tue, 23 Aug 2011 14:11:02 -0700 |
declare euclidean_simps [simp] at the point they are proved;
|
file | diff | annotate |
| Thu, 18 Aug 2011 13:36:58 -0700 |
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
|
file | diff | annotate |
| Wed, 10 Aug 2011 16:35:50 -0700 |
remove several redundant and unused theorems about derivatives
|
file | diff | annotate |
| Wed, 10 Aug 2011 14:10:52 -0700 |
simplify some proofs
|
file | diff | annotate |
| Tue, 09 Aug 2011 10:30:00 -0700 |
mark some redundant theorems as legacy
|
file | diff | annotate |
| Tue, 09 Aug 2011 08:53:12 -0700 |
Derivative.thy: more sensible subsection headings
|
file | diff | annotate |
| Tue, 09 Aug 2011 07:37:18 -0700 |
Derivative.thy: clean up formatting
|
file | diff | annotate |
| Mon, 08 Aug 2011 19:26:53 -0700 |
rename type 'a net to 'a filter, following standard mathematical terminology
|
file | diff | annotate |
| Thu, 09 Jun 2011 11:50:16 +0200 |
lemmas about right derivative and limits
|
file | diff | annotate |
| Mon, 14 Mar 2011 14:37:35 +0100 |
generalize infinite sums
|
file | diff | annotate |
| Sun, 13 Mar 2011 22:24:10 +0100 |
eliminated hard tabs;
|
file | diff | annotate |
| Tue, 22 Feb 2011 16:07:23 +0100 |
add name continuous_isCont to unnamed lemma
|
file | diff | annotate |
| Mon, 22 Nov 2010 10:34:33 +0100 |
Replace surj by abbreviation; remove surj_on.
|
file | diff | annotate |
| Mon, 13 Sep 2010 11:13:15 +0200 |
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 |
expand_fun_eq -> ext_iff
|
file | diff | annotate |
| Sun, 04 Jul 2010 09:26:30 -0700 |
generalize some lemmas about derivatives
|
file | diff | annotate |
| Wed, 30 Jun 2010 21:29:58 -0700 |
generalize some lemmas about derivatives
|
file | diff | annotate |
| Wed, 30 Jun 2010 19:00:15 -0700 |
generalize more euclidean_space lemmas
|
file | diff | annotate |
| Mon, 28 Jun 2010 15:32:26 +0200 |
inner_simps is not enough, need also local facts
|
file | diff | annotate |
| Mon, 21 Jun 2010 19:33:51 +0200 |
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
|
file | diff | annotate |
| Tue, 11 May 2010 19:21:05 +0200 |
Removed usage of normalizating locales.
|
file | diff | annotate |
| Fri, 07 May 2010 09:59:24 +0200 |
prefix normalizing replaces class_semiring
|
file | diff | annotate |
| Thu, 06 May 2010 23:11:57 +0200 |
former free-floating field_comp_conv now in structure Normalizer
|
file | diff | annotate |
| Thu, 29 Apr 2010 11:41:04 -0700 |
define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
|
file | diff | annotate |
| Wed, 28 Apr 2010 22:20:59 -0700 |
remove redundant lemma vector_dist_norm
|
file | diff | annotate |
| Wed, 28 Apr 2010 15:05:45 -0700 |
move operator norm stuff to new theory file
|
file | diff | annotate |
| Mon, 26 Apr 2010 16:28:58 -0700 |
more lemmas to Vec1.thy
|
file | diff | annotate |
| Mon, 26 Apr 2010 15:51:10 -0700 |
simplify proof
|
file | diff | annotate |
| Mon, 26 Apr 2010 15:44:54 -0700 |
move more lemmas into Vec1.thy
|
file | diff | annotate |
| Mon, 26 Apr 2010 15:22:03 -0700 |
move proof of Fashoda meet theorem into separate file
|
file | diff | annotate |
| Mon, 26 Apr 2010 12:19:57 -0700 |
move definitions and theorems for type real^1 to separate theory file
|
file | diff | annotate |
| Mon, 26 Apr 2010 09:45:22 -0700 |
merged
|
file | diff | annotate |
| Mon, 26 Apr 2010 09:21:25 -0700 |
fix lots of looping simp calls and other warnings
|
file | diff | annotate |
| Mon, 26 Apr 2010 11:34:19 +0200 |
dropped group_simps, ring_simps, field_eq_simps
|
file | diff | annotate |
| Sat, 24 Apr 2010 13:31:52 -0700 |
document generation for Multivariate_Analysis
|
file | diff | annotate |
| Tue, 02 Mar 2010 21:32:37 +0100 |
replaced \<bullet> with inner
|
file | diff | annotate |
| Thu, 18 Feb 2010 22:11:19 +0100 |
Equivalence between DERIV and one-dimensional derivation in Multivariate-Analysis
|
file | diff | annotate |
| Wed, 17 Feb 2010 18:33:45 +0100 |
Added integration to Multivariate-Analysis (upto FTC)
|
file | diff | annotate |
| Fri, 05 Feb 2010 14:33:50 +0100 |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
file | diff | annotate |
| Mon, 01 Feb 2010 14:12:12 +0100 |
Removed explicit type annotations
|
file | diff | annotate |
| Mon, 25 Jan 2010 16:56:24 +0100 |
Replaced vec1 and dest_vec1 by abbreviation.
|
file | diff | annotate |
| Fri, 15 Jan 2010 08:27:21 +0100 |
spurious proof failure
|
file | diff | annotate |
| Thu, 07 Jan 2010 18:56:39 +0100 |
finite annotation on cartesian product is now implicit.
|
file | diff | annotate |
| Wed, 06 Jan 2010 13:07:30 +0100 |
Made finite cartesian products finite
|
file | diff | annotate |
| Sun, 29 Nov 2009 22:27:47 -0800 |
make proof use only abstract properties of eventually
|
file | diff | annotate |
| Thu, 19 Nov 2009 11:57:30 +0100 |
Added the contributions of Robert Himmelmann to CONTRIBUTIONS and NEWS
|
file | diff | annotate |
| Thu, 19 Nov 2009 11:51:37 +0100 |
Renamed vector_less_eq_def to the more usual name vector_le_def.
|
file | diff | annotate |
| Tue, 17 Nov 2009 18:52:30 +0100 |
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
|
file | diff | annotate |