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
|
Wed, 30 Jun 2010 21:29:58 -0700 |
huffman |
generalize some lemmas about derivatives
|
file |
diff |
annotate
|
Wed, 30 Jun 2010 19:00:15 -0700 |
huffman |
generalize more euclidean_space lemmas
|
file |
diff |
annotate
|
Mon, 28 Jun 2010 15:32:26 +0200 |
haftmann |
inner_simps is not enough, need also local facts
|
file |
diff |
annotate
|
Mon, 21 Jun 2010 19:33:51 +0200 |
hoelzl |
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 |
hoelzl |
Removed usage of normalizating locales.
|
file |
diff |
annotate
|
Fri, 07 May 2010 09:59:24 +0200 |
haftmann |
prefix normalizing replaces class_semiring
|
file |
diff |
annotate
|
Thu, 06 May 2010 23:11:57 +0200 |
haftmann |
former free-floating field_comp_conv now in structure Normalizer
|
file |
diff |
annotate
|
Thu, 29 Apr 2010 11:41:04 -0700 |
huffman |
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 |
huffman |
remove redundant lemma vector_dist_norm
|
file |
diff |
annotate
|
Wed, 28 Apr 2010 15:05:45 -0700 |
huffman |
move operator norm stuff to new theory file
|
file |
diff |
annotate
|
Mon, 26 Apr 2010 16:28:58 -0700 |
huffman |
more lemmas to Vec1.thy
|
file |
diff |
annotate
|
Mon, 26 Apr 2010 15:51:10 -0700 |
huffman |
simplify proof
|
file |
diff |
annotate
|
Mon, 26 Apr 2010 15:44:54 -0700 |
huffman |
move more lemmas into Vec1.thy
|
file |
diff |
annotate
|
Mon, 26 Apr 2010 15:22:03 -0700 |
huffman |
move proof of Fashoda meet theorem into separate file
|
file |
diff |
annotate
|
Mon, 26 Apr 2010 12:19:57 -0700 |
huffman |
move definitions and theorems for type real^1 to separate theory file
|
file |
diff |
annotate
|
Mon, 26 Apr 2010 09:45:22 -0700 |
huffman |
merged
|
file |
diff |
annotate
|
Mon, 26 Apr 2010 09:21:25 -0700 |
huffman |
fix lots of looping simp calls and other warnings
|
file |
diff |
annotate
|
Mon, 26 Apr 2010 11:34:19 +0200 |
haftmann |
dropped group_simps, ring_simps, field_eq_simps
|
file |
diff |
annotate
|
Sat, 24 Apr 2010 13:31:52 -0700 |
huffman |
document generation for Multivariate_Analysis
|
file |
diff |
annotate
|
Tue, 02 Mar 2010 21:32:37 +0100 |
himmelma |
replaced \<bullet> with inner
|
file |
diff |
annotate
|
Thu, 18 Feb 2010 22:11:19 +0100 |
himmelma |
Equivalence between DERIV and one-dimensional derivation in Multivariate-Analysis
|
file |
diff |
annotate
|
Wed, 17 Feb 2010 18:33:45 +0100 |
himmelma |
Added integration to Multivariate-Analysis (upto FTC)
|
file |
diff |
annotate
|
Fri, 05 Feb 2010 14:33:50 +0100 |
haftmann |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
file |
diff |
annotate
|
Mon, 01 Feb 2010 14:12:12 +0100 |
himmelma |
Removed explicit type annotations
|
file |
diff |
annotate
|
Mon, 25 Jan 2010 16:56:24 +0100 |
hoelzl |
Replaced vec1 and dest_vec1 by abbreviation.
|
file |
diff |
annotate
|
Fri, 15 Jan 2010 08:27:21 +0100 |
haftmann |
spurious proof failure
|
file |
diff |
annotate
|