src/HOL/NSA/NSComplex.thy
2013-03-26 hoelzl HOL-NSA should only import Complex_Main
2012-10-19 webertj Renamed {left,right}_distrib to distrib_{right,left}.
2012-03-25 huffman merged fork with new numeral representation (see NEWS)
2011-09-08 huffman remove unnecessary intermediate lemmas
2011-09-08 huffman remove obsolete intermediate lemma complex_inverse_complex_split
2011-09-08 huffman simplify proof of lemma DeMoivre, removing unnecessary intermediate lemma
2011-09-06 huffman remove redundant lemmas i_mult_eq and i_mult_eq2 in favor of i_squared
2011-09-04 huffman remove redundant lemmas expi_add and expi_zero
2011-04-23 wenzelm modernized specifications;
2011-03-13 wenzelm tuned headers;
2010-12-29 wenzelm explicit file specifications -- avoid secondary load path;
2010-07-12 haftmann dropped superfluous [code del]s
2010-02-08 haftmann renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
2009-12-19 huffman rename equals_zero_I to minus_unique (keep old name too)
2009-04-28 haftmann power constraint needed, though
2009-04-28 haftmann stripped class recpower further
2008-10-10 haftmann `code func` now just `code`
2008-07-03 huffman move nonstandard analysis theories to NSA directory
less more (0) tip