src/HOL/NSA/HTranscendental.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-13 immler 2014-10-13 relaxed class constraints for exp
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-03-18 hoelzl 2014-03-18 fix HOL-NSA; move lemmas
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-08-18 wenzelm 2013-08-18 more symbols;
2011-08-19 huffman 2011-08-19 remove redundant lemma exp_ln_eq in favor of ln_unique
2010-07-19 haftmann 2010-07-19 diff_minus subsumes diff_def
2009-05-27 huffman 2009-05-27 add constants sin_coeff, cos_coeff
2009-03-04 huffman 2009-03-04 declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
2008-07-03 huffman 2008-07-03 move nonstandard analysis theories to NSA directory