| Wed, 11 Apr 2007 04:13:06 +0200 |
huffman |
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
|
file |
diff |
annotate
|
| Tue, 10 Apr 2007 22:01:19 +0200 |
huffman |
new LIM/isCont lemmas for abs, of_real, and power
|
file |
diff |
annotate
|
| Sun, 08 Apr 2007 17:54:52 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| Wed, 14 Mar 2007 21:40:28 +0100 |
huffman |
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
|
file |
diff |
annotate
|
| Wed, 13 Dec 2006 00:07:13 +0100 |
huffman |
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
|
file |
diff |
annotate
|
| Tue, 12 Dec 2006 07:13:06 +0100 |
huffman |
cleaned up; generalized some proofs
|
file |
diff |
annotate
|
| Sun, 10 Dec 2006 07:12:26 +0100 |
nipkow |
Modified lattice locale
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Thu, 16 Nov 2006 20:19:50 +0100 |
huffman |
add lemmas LIM_zero_iff, LIM_norm_zero_iff
|
file |
diff |
annotate
|
| Fri, 10 Nov 2006 00:46:00 +0100 |
huffman |
added bounded_linear and bounded_bilinear locales
|
file |
diff |
annotate
|
| Thu, 09 Nov 2006 00:19:16 +0100 |
huffman |
added LIM_norm and related lemmas
|
file |
diff |
annotate
|
| Wed, 08 Nov 2006 02:13:02 +0100 |
huffman |
LIM_compose -> isCont_LIM_compose;
|
file |
diff |
annotate
|
| Sat, 04 Nov 2006 00:12:06 +0100 |
huffman |
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
|
file |
diff |
annotate
|
| Wed, 01 Nov 2006 17:57:02 +0100 |
huffman |
move DERIV_sumr from Series.thy to Lim.thy
|
file |
diff |
annotate
|
| Wed, 01 Nov 2006 17:14:16 +0100 |
huffman |
generalize type of lemma isCont_Id
|
file |
diff |
annotate
|
| Sun, 01 Oct 2006 03:07:12 +0200 |
huffman |
generalize more DERIV proofs
|
file |
diff |
annotate
|
| Sat, 30 Sep 2006 20:54:34 +0200 |
huffman |
generalize proofs of DERIV_isCont and DERIV_mult
|
file |
diff |
annotate
|
| Sat, 30 Sep 2006 19:41:06 +0200 |
huffman |
generalized some DERIV proofs
|
file |
diff |
annotate
|
| Sat, 30 Sep 2006 18:04:28 +0200 |
huffman |
add scaleR lemmas
|
file |
diff |
annotate
|
| Sat, 30 Sep 2006 17:36:55 +0200 |
huffman |
generalize type of DERIV
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 06:21:06 +0200 |
huffman |
more reorganizing sections
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 04:03:43 +0200 |
huffman |
reorganize sections
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 02:50:07 +0200 |
huffman |
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 01:26:28 +0200 |
huffman |
generalize type of is(NS)UCont
|
file |
diff |
annotate
|
| Sun, 24 Sep 2006 06:54:39 +0200 |
huffman |
generalize types of lim and nslim
|
file |
diff |
annotate
|
| Thu, 21 Sep 2006 03:17:51 +0200 |
huffman |
removed division_by_zero class requirements from several lemmas
|
file |
diff |
annotate
|
| Wed, 20 Sep 2006 07:44:34 +0200 |
huffman |
change section to subsection
|
file |
diff |
annotate
|
| Mon, 18 Sep 2006 07:48:07 +0200 |
huffman |
replace (x + - y) with (x - y)
|
file |
diff |
annotate
|
| Sun, 17 Sep 2006 16:44:05 +0200 |
huffman |
generalize type of (NS)LIM to work on functions with vector space domain types
|
file |
diff |
annotate
|
| Sat, 16 Sep 2006 02:40:00 +0200 |
huffman |
generalized types of many constants to work over arbitrary vector spaces;
|
file |
diff |
annotate
|