src/HOL/Complex/CLim.thy
Tue, 22 May 2007 19:58:54 +0200 huffman removed redundant lemmas
Tue, 22 May 2007 07:29:49 +0200 huffman rename lemmas LIM_ident, isCont_ident, DERIV_ident
Tue, 15 May 2007 08:10:31 +0200 huffman minimize imports
Wed, 09 May 2007 01:26:04 +0200 huffman hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
Wed, 13 Dec 2006 21:25:56 +0100 huffman added lemmas about hRe, hIm, HComplex; removed all uses of star_n
Wed, 13 Dec 2006 19:39:48 +0100 huffman remove references to star_n
Tue, 12 Dec 2006 17:29:26 +0100 huffman removed redundant constants and lemmas
Fri, 17 Nov 2006 02:20:03 +0100 wenzelm more robust syntax for definition/abbreviation/notation;
Thu, 28 Sep 2006 01:26:28 +0200 huffman generalize type of is(NS)UCont
Wed, 27 Sep 2006 18:34:26 +0200 huffman remove redundant lemmas
Thu, 21 Sep 2006 16:45:53 +0200 huffman changed constants into abbreviations; shortened proofs
Mon, 18 Sep 2006 07:48:07 +0200 huffman replace (x + - y) with (x - y)
Sun, 17 Sep 2006 02:56:25 +0200 huffman removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
Sat, 16 Sep 2006 02:40:00 +0200 huffman generalized types of many constants to work over arbitrary vector spaces;
Wed, 26 Jul 2006 19:23:04 +0200 webertj linear arithmetic splits certain operators (e.g. min, max, abs)
less more (0) -15 tip