src/HOL/Complex/NSComplex.thy
Wed, 30 May 2007 01:53:38 +0200 huffman renamed some lemmas in Complex.thy
Mon, 14 May 2007 18:48:24 +0200 huffman move lemmas to RealPow.thy; tuned proofs
Thu, 10 May 2007 03:11:03 +0200 huffman remove redundant lemmas
Thu, 10 May 2007 03:07:26 +0200 huffman lemmas iszero_(h)complex_number_of are no longer needed
Wed, 09 May 2007 18:26:40 +0200 huffman remove redundant lemmas
Wed, 09 May 2007 01:26:04 +0200 huffman hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
Tue, 08 May 2007 05:06:54 +0200 huffman remove redundant lemmas
Fri, 13 Apr 2007 01:06:12 +0200 huffman minimize imports
Sat, 16 Dec 2006 19:37:07 +0100 huffman hypreal_of_hypnat abbreviates more general of_hypnat
Thu, 14 Dec 2006 19:15:16 +0100 huffman generalized type of hyperpow; removed hcpow
Thu, 14 Dec 2006 18:10:38 +0100 huffman redefine hSuc as *f* Suc, and move to HyperNat.thy
Wed, 13 Dec 2006 21:25:56 +0100 huffman added lemmas about hRe, hIm, HComplex; removed all uses of star_n
Fri, 17 Nov 2006 02:20:03 +0100 wenzelm more robust syntax for definition/abbreviation/notation;
Wed, 27 Sep 2006 07:09:19 +0200 huffman hypreal_of_nat abbreviates of_nat
Wed, 27 Sep 2006 05:19:24 +0200 huffman convert more proofs to transfer principle
Sun, 17 Sep 2006 02:53:36 +0200 huffman hcmod abbreviates hnorm :: hcomplex => hypreal
Wed, 06 Sep 2006 13:48:02 +0200 haftmann got rid of Numeral.bin type
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
Wed, 14 Sep 2005 01:47:06 +0200 huffman removed duplicated lemmas; convert more proofs to transfer principle
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 01:49:49 +0200 huffman replace type hcomplex with complex star
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, 15 Dec 2004 17:32:40 +0100 paulson removal of archaic Abs/Rep proofs
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
less more (0) -50 -30 tip