src/HOL/Hyperreal/HyperPow.thy
Thu, 14 Dec 2006 21:33:47 +0100 huffman prove hyperpow_realpow using transfer
Thu, 14 Dec 2006 19:15:16 +0100 huffman generalized type of hyperpow; removed hcpow
Fri, 17 Nov 2006 02:20:03 +0100 wenzelm more robust syntax for definition/abbreviation/notation;
Wed, 08 Nov 2006 23:11:13 +0100 wenzelm moved theories Parity, GCD, Binomial to Library;
Wed, 27 Sep 2006 07:09:19 +0200 huffman hypreal_of_nat abbreviates of_nat
Thu, 14 Sep 2006 21:42:21 +0200 huffman generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
Fri, 02 Jun 2006 23:22:29 +0200 wenzelm misc cleanup;
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
Mon, 12 Sep 2005 23:14:41 +0200 huffman added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
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
Wed, 27 Jul 2005 11:28:18 +0200 paulson removed the dependence on abs_mult
Mon, 21 Feb 2005 15:04:10 +0100 nipkow comprehensive cleanup, replacing sumr by setsum
Thu, 02 Dec 2004 11:42:01 +0100 nipkow Added "ALL x > y" and relatives.
Tue, 05 Oct 2004 15:30:50 +0200 paulson new simprules for abs and for things like a/b<1
Wed, 01 Sep 2004 15:04:01 +0200 paulson new "respects" syntax for quotienting
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
Thu, 24 Jun 2004 17:52:02 +0200 paulson replaced monomorphic abs definitions by abs_if
Mon, 15 Mar 2004 10:46:19 +0100 paulson heavy tidying
Mon, 08 Mar 2004 11:12:06 +0100 paulson generic theorems about exponentials; general tidying up
Fri, 05 Mar 2004 15:18:59 +0100 paulson Conversion of Poly to Isar script, and other tidying of HOL/Hyperreal
Sun, 15 Feb 2004 10:46:37 +0100 paulson Polymorphic treatment of binary arithmetic using axclasses
Tue, 10 Feb 2004 12:02:11 +0100 paulson generic of_nat and of_int functions, and generalization of iszero
Mon, 02 Feb 2004 12:23:46 +0100 paulson Conversion of HyperNat to Isar format and its declaration as a semiring
Fri, 09 Jan 2004 10:46:18 +0100 paulson Defining the type class "ringpower" and deleting superseded theorems for
Mon, 08 Oct 2001 15:23:20 +0200 wenzelm sane numerals (stage 3): provide generic "1" on all number types;
Tue, 09 Jan 2001 15:32:27 +0100 nipkow *** empty log message ***
Fri, 05 Jan 2001 18:48:18 +0100 nipkow ^^ -> ```
Thu, 04 Jan 2001 10:23:01 +0100 paulson more tidying, especially to remove real_of_posnat
Sat, 30 Dec 2000 22:03:47 +0100 paulson separation of HOL-Hyperreal from HOL-Real
less more (0) tip