src/HOL/Hyperreal/HyperDef.thy
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 02:13:24 +0200 huffman added theorem hypreal_inverse2
Tue, 06 Sep 2005 23:16:48 +0200 huffman replace type hypreal with real star
Tue, 06 Sep 2005 19:22:31 +0200 huffman reimplement Filter.thy with locales
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Mon, 21 Feb 2005 15:04:10 +0100 nipkow comprehensive cleanup, replacing sumr by setsum
Wed, 15 Dec 2004 17:32:40 +0100 paulson removal of archaic Abs/Rep proofs
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, 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
Sun, 11 Jul 2004 20:33:22 +0200 wenzelm local_cla/simpset_of;
less more (0) -15 tip