src/HOL/Hyperreal/NSA.thy
Sun, 17 Sep 2006 16:44:51 +0200 huffman add type constraint to otherwise looping iff rule
Sat, 16 Sep 2006 19:12:03 +0200 huffman define new constant of_real for class real_algebra_1;
Sat, 16 Sep 2006 02:40:00 +0200 huffman generalized types of many constants to work over arbitrary vector spaces;
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
Wed, 06 Sep 2006 13:48:02 +0200 haftmann got rid of Numeral.bin type
Wed, 30 Aug 2006 03:19:08 +0200 webertj lin_arith_prover: splitting reverted because of performance loss
Wed, 23 Aug 2006 21:57:43 +0200 huffman speed up some proofs
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, 16 Sep 2005 01:34:53 +0200 huffman fix names in hypreal_arith.ML
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;
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
Tue, 12 Jul 2005 17:56:03 +0200 avigad added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
Mon, 21 Feb 2005 15:04:10 +0100 nipkow comprehensive cleanup, replacing sumr by setsum
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
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, 24 Jun 2004 17:52:02 +0200 paulson replaced monomorphic abs definitions by abs_if
Thu, 22 Apr 2004 12:11:17 +0200 wenzelm constdefs: proper order;
Wed, 14 Apr 2004 14:13:05 +0200 kleing use more symbols in HTML output
Fri, 19 Mar 2004 10:51:03 +0100 paulson conversion of Hyperreal/Lim to new-style
Mon, 15 Mar 2004 10:46:19 +0100 paulson heavy tidying
Thu, 04 Mar 2004 12:06:07 +0100 paulson new material from Avigad, and simplified treatment of division by 0
Mon, 01 Mar 2004 11:52:59 +0100 paulson converted Hyperreal/HTranscendental to Isar script
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
Thu, 29 Jan 2004 16:51:17 +0100 paulson simplifications in the hyperreals
Fri, 09 Nov 2001 00:09:47 +0100 wenzelm eliminated old "symbols" syntax, use "xsymbols" instead;
Tue, 16 Jan 2001 12:20:52 +0100 paulson renamings: real_of_nat, real_of_int -> (overloaded) real
Sat, 30 Dec 2000 22:03:47 +0100 paulson separation of HOL-Hyperreal from HOL-Real
less more (0) tip