| Wed, 13 Dec 2006 00:07:13 +0100 |
huffman |
generalized some lemmas; removed redundant lemmas; cleaned up some proofs
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Wed, 01 Nov 2006 16:48:58 +0100 |
huffman |
new proof of Bseq_NSbseq using transfer
|
file |
diff |
annotate
|
| Mon, 02 Oct 2006 21:30:05 +0200 |
huffman |
add axclass banach for complete normed vector spaces
|
file |
diff |
annotate
|
| Mon, 02 Oct 2006 19:57:02 +0200 |
huffman |
remove unused Cauchy_Bseq lemmas
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 00:57:36 +0200 |
huffman |
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
|
file |
diff |
annotate
|
| Wed, 27 Sep 2006 21:44:38 +0200 |
huffman |
reorganized HNatInfinite proofs; simplified and renamed some lemmas
|
file |
diff |
annotate
|
| Wed, 27 Sep 2006 05:39:29 +0200 |
huffman |
move star_of_norm from SEQ.thy to NSA.thy
|
file |
diff |
annotate
|
| Sun, 24 Sep 2006 08:22:21 +0200 |
huffman |
reorganized subsection headings
|
file |
diff |
annotate
|
| Sun, 24 Sep 2006 07:18:16 +0200 |
huffman |
moved SEQ_Infinitesimal from SEQ to HyperNat
|
file |
diff |
annotate
|
| Sun, 24 Sep 2006 06:54:39 +0200 |
huffman |
generalize types of lim and nslim
|
file |
diff |
annotate
|
| Sun, 24 Sep 2006 04:16:28 +0200 |
huffman |
add lemma convergent_Cauchy
|
file |
diff |
annotate
|
| Fri, 22 Sep 2006 23:19:45 +0200 |
huffman |
added lemmas about LIMSEQ and norm; simplified some proofs
|
file |
diff |
annotate
|
| Fri, 22 Sep 2006 16:25:15 +0200 |
huffman |
define constants with THE instead of SOME
|
file |
diff |
annotate
|
| Thu, 21 Sep 2006 03:17:51 +0200 |
huffman |
removed division_by_zero class requirements from several lemmas
|
file |
diff |
annotate
|
| Mon, 18 Sep 2006 07:48:07 +0200 |
huffman |
replace (x + - y) with (x - y)
|
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
|
| Wed, 23 Aug 2006 22:12:54 +0200 |
huffman |
generalize proof of SUP_rabs_subseq
|
file |
diff |
annotate
|
| Wed, 26 Jul 2006 19:23:04 +0200 |
webertj |
linear arithmetic splits certain operators (e.g. min, max, abs)
|
file |
diff |
annotate
|
| Fri, 02 Jun 2006 23:22:29 +0200 |
wenzelm |
misc cleanup;
|
file |
diff |
annotate
|
| Thu, 05 Jan 2006 22:29:55 +0100 |
wenzelm |
replaced swap by contrapos_np;
|
file |
diff |
annotate
|
| Fri, 16 Sep 2005 20:30:44 +0200 |
huffman |
add header
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 23:46:22 +0200 |
huffman |
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
|
file |
diff |
annotate
|
| Fri, 09 Sep 2005 19:34:22 +0200 |
huffman |
starfun, starset, and other functions on NS types are now polymorphic;
|
file |
diff |
annotate
|
| Wed, 07 Sep 2005 00:48:50 +0200 |
huffman |
replace type hypnat with nat star
|
file |
diff |
annotate
|
| Tue, 06 Sep 2005 23:16:48 +0200 |
huffman |
replace type hypreal with real star
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 19:49:07 +0200 |
avigad |
Additions to the Real (and Hyperreal) libraries:
|
file |
diff |
annotate
|
| Mon, 21 Feb 2005 15:04:10 +0100 |
nipkow |
comprehensive cleanup, replacing sumr by setsum
|
file |
diff |
annotate
|
| Thu, 02 Dec 2004 11:42:01 +0100 |
nipkow |
Added "ALL x > y" and relatives.
|
file |
diff |
annotate
|
| Tue, 23 Nov 2004 15:32:11 +0100 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Tue, 19 Oct 2004 18:18:45 +0200 |
paulson |
converted some induct_tac to induct
|
file |
diff |
annotate
|
| Tue, 12 Oct 2004 11:48:21 +0200 |
paulson |
tweaks concerned with poly bug-fixing
|
file |
diff |
annotate
|
| Mon, 11 Oct 2004 07:42:22 +0200 |
nipkow |
Proofs needed to be updated because induction now preserves name of
|
file |
diff |
annotate
|
| Tue, 05 Oct 2004 15:30:50 +0200 |
paulson |
new simprules for abs and for things like a/b<1
|
file |
diff |
annotate
|
| Fri, 01 Oct 2004 11:53:31 +0200 |
paulson |
tweaking of arithmetic proofs
|
file |
diff |
annotate
|
| Wed, 18 Aug 2004 11:09:40 +0200 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
| Mon, 16 Aug 2004 14:22:27 +0200 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
| Tue, 03 Aug 2004 13:48:00 +0200 |
paulson |
new simprules Int_subset_iff and Un_subset_iff
|
file |
diff |
annotate
|
| Thu, 29 Jul 2004 16:14:42 +0200 |
paulson |
removed some [iff] declarations from RealDef.thy, concerning inequalities
|
file |
diff |
annotate
|
| Wed, 28 Jul 2004 16:26:27 +0200 |
paulson |
conversion of SEQ.ML to Isar script
|
file |
diff |
annotate
|
| Fri, 07 Feb 2003 16:40:23 +0100 |
nipkow |
(*f -> ( *f because of new comments
|
file |
diff |
annotate
|
| Fri, 02 Nov 2001 17:55:24 +0100 |
paulson |
Numerals and simprocs for types real and hypreal. The abstract
|
file |
diff |
annotate
|
| Fri, 05 Oct 2001 21:52:39 +0200 |
wenzelm |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
|
file |
diff |
annotate
|
| Sat, 30 Dec 2000 22:03:47 +0100 |
paulson |
separation of HOL-Hyperreal from HOL-Real
|
file |
diff |
annotate
|