src/HOL/Complex/CStar.thy
2006-12-14 huffman 2006-12-14 generalized type of hyperpow; removed hcpow
2006-12-13 huffman 2006-12-13 added lemmas about hRe, hIm, HComplex; removed all uses of star_n
2006-12-13 huffman 2006-12-13 SComplex abbreviates Standard
2006-09-27 huffman 2006-09-27 remove redundant lemmas
2006-09-17 huffman 2006-09-17 removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
2006-06-02 wenzelm 2006-06-02 misc cleanup;
2005-09-09 huffman 2005-09-09 starfun, starset, and other functions on NS types are now polymorphic; many similar theorems have been generalized and merged; (star_n X) replaces (Abs_star(starrel `` {X})); many proofs have been simplified with the transfer tactic.
2005-09-07 huffman 2005-09-07 replace type hcomplex with complex star
2005-09-06 huffman 2005-09-06 replace type hypreal with real star
2005-09-06 huffman 2005-09-06 fix proof
2004-10-07 paulson 2004-10-07 simplification tweaks for better arithmetic reasoning
2004-09-01 paulson 2004-09-01 new "respects" syntax for quotienting
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-03-15 paulson 2004-03-15 heavy tidying
2004-03-04 paulson 2004-03-04 new material from Avigad, and simplified treatment of division by 0
2004-02-21 paulson 2004-02-21 conversion of Complex/CStar to Isar script
2003-05-05 paulson 2003-05-05 new session Complex for the complex numbers