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