| Tue, 29 May 2007 18:31:30 +0200 |
huffman |
cleaned up some proofs
|
file |
diff |
annotate
|
| Tue, 29 May 2007 17:37:04 +0200 |
huffman |
add bounded_linear lemmas
|
file |
diff |
annotate
|
| Sun, 27 May 2007 20:04:02 +0200 |
huffman |
new proof of Cauchy product formula for series
|
file |
diff |
annotate
|
| Wed, 23 May 2007 19:23:22 +0200 |
huffman |
add lemma complete_algebra_summable_geometric
|
file |
diff |
annotate
|
| Thu, 17 May 2007 21:51:32 +0200 |
huffman |
avoid using redundant lemmas from RealDef.thy
|
file |
diff |
annotate
|
| Mon, 14 May 2007 09:11:30 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| Mon, 07 May 2007 23:07:04 +0200 |
huffman |
clean up RealVector classes
|
file |
diff |
annotate
|
| Tue, 17 Apr 2007 00:33:49 +0200 |
huffman |
lemma geometric_sum no longer needs class division_by_zero
|
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 17:57:02 +0100 |
huffman |
move DERIV_sumr from Series.thy to Lim.thy
|
file |
diff |
annotate
|
| Mon, 02 Oct 2006 23:15:35 +0200 |
huffman |
generalize summability lemmas using class banach
|
file |
diff |
annotate
|
| Sat, 30 Sep 2006 17:10:55 +0200 |
huffman |
add type annotations for DERIV
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 23:42:43 +0200 |
wenzelm |
fixed translations: CONST;
|
file |
diff |
annotate
|
| Sun, 24 Sep 2006 05:49:50 +0200 |
huffman |
generalized types of sums, summable, and suminf
|
file |
diff |
annotate
|
| Sun, 24 Sep 2006 04:00:03 +0200 |
huffman |
add proof of summable_LIMSEQ_zero
|
file |
diff |
annotate
|
| Sun, 24 Sep 2006 03:38:36 +0200 |
huffman |
change definitions from SOME to THE
|
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, 30 Aug 2006 03:19:08 +0200 |
webertj |
lin_arith_prover: splitting reverted because of performance loss
|
file |
diff |
annotate
|
| Wed, 23 Aug 2006 23:40:47 +0200 |
huffman |
speed up proof of summable_Cauchy
|
file |
diff |
annotate
|
| Sat, 29 Jul 2006 13:15:12 +0200 |
webertj |
lin_arith_prover splits certain operators (e.g. min, max, abs)
|
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
|
| Fri, 17 Mar 2006 10:04:27 +0100 |
ballarin |
Renamed setsum_mult to setsum_right_distrib.
|
file |
diff |
annotate
|
| Sun, 19 Feb 2006 13:21:32 +0100 |
kleing |
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
|
file |
diff |
annotate
|
| Fri, 26 Aug 2005 10:01:06 +0200 |
ballarin |
Lemmas on dvd, power and finite summation added or strengthened.
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 19:49:07 +0200 |
avigad |
Additions to the Real (and Hyperreal) libraries:
|
file |
diff |
annotate
|
| Thu, 07 Jul 2005 12:39:17 +0200 |
nipkow |
linear arithmetic now takes "&" in assumptions apart.
|
file |
diff |
annotate
|
| Wed, 02 Mar 2005 12:06:15 +0100 |
nipkow |
another reorganization of setsums and intervals
|
file |
diff |
annotate
|
| Wed, 23 Feb 2005 10:23:22 +0100 |
nipkow |
suminf -> \<Sum>
|
file |
diff |
annotate
|
| Tue, 22 Feb 2005 10:54:30 +0100 |
nipkow |
more setsum tuning
|
file |
diff |
annotate
|
| Mon, 21 Feb 2005 19:23:46 +0100 |
nipkow |
more fine tuniung
|
file |
diff |
annotate
|
| Mon, 21 Feb 2005 15:04:10 +0100 |
nipkow |
comprehensive cleanup, replacing sumr by setsum
|
file |
diff |
annotate
|
| Fri, 18 Feb 2005 15:20:27 +0100 |
nipkow |
continued eliminating sumr
|
file |
diff |
annotate
|
| Fri, 18 Feb 2005 11:48:53 +0100 |
nipkow |
starting to get rid of sumr
|
file |
diff |
annotate
|
| Thu, 02 Dec 2004 11:42:01 +0100 |
nipkow |
Added "ALL x > y" and relatives.
|
file |
diff |
annotate
|
| Tue, 19 Oct 2004 18:18:45 +0200 |
paulson |
converted some induct_tac to induct
|
file |
diff |
annotate
|
| Thu, 07 Oct 2004 15:42:30 +0200 |
paulson |
simplification tweaks for better arithmetic reasoning
|
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
|
| 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
|
| Thu, 29 Jul 2004 16:14:42 +0200 |
paulson |
removed some [iff] declarations from RealDef.thy, concerning inequalities
|
file |
diff |
annotate
|
| Fri, 16 Jul 2004 17:31:44 +0200 |
nipkow |
Corrected TeX problems.
|
file |
diff |
annotate
|
| Thu, 15 Jul 2004 15:32:32 +0200 |
paulson |
redefining sumr to be a translation to setsum
|
file |
diff |
annotate
|
| Thu, 24 Jun 2004 17:52:02 +0200 |
paulson |
replaced monomorphic abs definitions by abs_if
|
file |
diff |
annotate
|
| Thu, 26 Feb 2004 17:08:23 +0100 |
paulson |
converted Hyperreal/Series to Isar script
|
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
|