src/HOL/Hyperreal/HSeries.thy
Wed, 02 Jul 2008 07:11:57 +0200 haftmann cleaned up some code generator configuration
Wed, 11 Apr 2007 04:13:06 +0200 huffman moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
Sat, 16 Dec 2006 19:37:07 +0100 huffman hypreal_of_hypnat abbreviates more general of_hypnat
Wed, 13 Dec 2006 23:15:39 +0100 huffman remove uses of star_n and FreeUltrafilterNat
Fri, 17 Nov 2006 02:20:03 +0100 wenzelm more robust syntax for definition/abbreviation/notation;
Mon, 09 Oct 2006 02:19:51 +0200 wenzelm attribute symmetric: zero_var_indexes;
Mon, 02 Oct 2006 23:15:35 +0200 huffman generalize summability lemmas using class banach
Sun, 24 Sep 2006 05:49:50 +0200 huffman generalized types of sums, summable, and suminf
Sun, 24 Sep 2006 03:38:36 +0200 huffman change definitions from SOME to THE
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.
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
Fri, 09 Sep 2005 19:34:22 +0200 huffman starfun, starset, and other functions on NS types are now polymorphic;
Wed, 07 Sep 2005 00:48:50 +0200 huffman replace type hypnat with nat star
Tue, 06 Sep 2005 23:16:48 +0200 huffman replace type hypreal with real star
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 11:48:53 +0100 nipkow starting to get rid of sumr
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, 15 Jul 2004 15:32:32 +0200 paulson redefining sumr to be a translation to setsum
Mon, 15 Mar 2004 10:46:19 +0100 paulson heavy tidying
Fri, 05 Mar 2004 15:18:59 +0100 paulson Conversion of Poly to Isar script, and other tidying of HOL/Hyperreal
Wed, 25 Feb 2004 16:22:36 +0100 paulson converted Hyperreal/HSeries to Isar script
Tue, 09 Jan 2001 15:32:27 +0100 nipkow *** empty log message ***
Fri, 05 Jan 2001 18:48:18 +0100 nipkow ^^ -> ```
Sat, 30 Dec 2000 22:03:47 +0100 paulson separation of HOL-Hyperreal from HOL-Real
less more (0) tip