src/HOL/NSA/NSComplex.thy
2015-04-11 paulson 2015-04-11 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
2015-03-16 paulson 2015-03-16 The factorial function, "fact", now has type "nat => 'a"
2015-03-09 paulson 2015-03-09 sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-10-26 haftmann 2014-10-26 eliminated redundancies; more simp rules
2014-05-07 hoelzl 2014-05-07 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-08-18 wenzelm 2013-08-18 more symbols;
2013-03-26 hoelzl 2013-03-26 HOL-NSA should only import Complex_Main
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2011-09-08 huffman 2011-09-08 remove unnecessary intermediate lemmas
2011-09-08 huffman 2011-09-08 remove obsolete intermediate lemma complex_inverse_complex_split
2011-09-07 huffman 2011-09-07 simplify proof of lemma DeMoivre, removing unnecessary intermediate lemma
2011-09-06 huffman 2011-09-06 remove redundant lemmas i_mult_eq and i_mult_eq2 in favor of i_squared
2011-09-04 huffman 2011-09-04 remove redundant lemmas expi_add and expi_zero
2011-04-23 wenzelm 2011-04-23 modernized specifications;
2011-03-13 wenzelm 2011-03-13 tuned headers;
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-02-08 haftmann 2010-02-08 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
2009-12-18 huffman 2009-12-18 rename equals_zero_I to minus_unique (keep old name too)
2009-04-28 haftmann 2009-04-28 power constraint needed, though
2009-04-28 haftmann 2009-04-28 stripped class recpower further
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-07-03 huffman 2008-07-03 move nonstandard analysis theories to NSA directory