src/HOL/Transcendental.thy
2016-05-13 wenzelm 2016-05-13 eliminated use of empty "assms";
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-04-12 immler 2016-04-12 added derivative of scaling in exponential function
2016-04-11 paulson 2016-04-11 lots of new theorems for multivariate analysis
2016-03-21 hoelzl 2016-03-21 add le_log_of_power and le_log2_of_power by Tobias Nipkow
2016-02-23 nipkow 2016-02-23 resolved conflict
2016-02-23 nipkow 2016-02-23 more canonical names
2016-02-23 paulson 2016-02-23 New and revised material for (multivariate) analysis
2016-02-22 paulson 2016-02-22 An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
2016-02-17 haftmann 2016-02-17 generalized some lemmas; moved some lemmas in more appropriate places; deleted potentially dangerous simp rule
2016-01-06 hoelzl 2016-01-06 add the proof of the central limit theorem
2016-01-04 eberlm 2016-01-04 Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
2015-12-30 wenzelm 2015-12-30 more symbols;
2015-12-30 wenzelm 2015-12-30 more symbols;
2015-12-29 wenzelm 2015-12-29 more symbols;
2015-12-28 wenzelm 2015-12-28 prefer symbols for "abs";
2015-12-27 wenzelm 2015-12-27 prefer symbols for "floor", "ceiling";
2015-12-21 hoelzl 2015-12-21 Transcendental: use [simp]-canonical form - (pi/2)
2015-12-09 paulson 2015-12-09 sorted out eventually_mono
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-12-01 paulson 2015-12-01 Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
2015-11-23 paulson 2015-11-23 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
2015-11-17 paulson 2015-11-17 Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
2015-11-13 paulson 2015-11-13 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-11-10 paulson 2015-11-10 Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
2015-11-02 eberlm 2015-11-02 Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
2015-11-02 eberlm 2015-11-02 Rounding function, uniform limits, cotangent, binomial identities
2015-10-29 eberlm 2015-10-29 added many small lemmas about setsum/setprod/powr/...
2015-10-26 paulson 2015-10-26 new lemmas about topology, etc., for Cauchy integral formula
2015-09-30 paulson 2015-09-30 real_of_nat_Suc is now a simprule
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-08-31 wenzelm 2015-08-31 prefer symbols;
2015-08-06 haftmann 2015-08-06 slight cleanup of lemmas
2015-07-20 paulson 2015-07-20 new material for multivariate analysis, etc.
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-07-14 hoelzl 2015-07-14 generalized filtermap_homeomorph to filtermap_fun_inverse; add eventually_at_top/bot_not_equal
2015-07-08 haftmann 2015-07-08 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
2015-05-25 wenzelm 2015-05-25 merged, resolving conflicts in Admin/isatest/settings/afp-poly and src/HOL/Tools/Nitpick/nitpick_model.ML;
2015-05-03 wenzelm 2015-05-03 tuned;
2015-05-07 hoelzl 2015-05-07 generalized tends over powr; added DERIV rule for powr
2015-04-30 paulson 2015-04-30 tidying some messy proofs
2015-04-29 paulson 2015-04-29 Tidying. Improved simplification for numerals, esp in exponents.
2015-04-28 paulson 2015-04-28 New material about complex transcendental functions (especially Ln, Arg) and polynomials
2015-04-21 paulson 2015-04-21 New material, mostly about limits. Consolidation.
2015-04-12 hoelzl 2015-04-12 move filters to their own theory
2015-04-12 hoelzl 2015-04-12 fix latex in Transcendental
2015-04-11 paulson 2015-04-11 Complex roots of unity. Better definition of ln for complex numbers. Used [code del] to stop code generation for powr.
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-04-01 paulson 2015-04-01 arcsin and arccos lemmas
2015-03-31 haftmann 2015-03-31 given up separate type classes demanding `inverse 0 = 0`
2015-03-31 paulson 2015-03-31 rationalised and generalised some theorems concerning abs and x^2.
2015-03-31 paulson 2015-03-31 New material and binomial fix
2015-03-19 paulson 2015-03-19 New material for complex sin, cos, tan, Ln, also some reorganisation
2015-03-18 paulson 2015-03-18 new HOL Light material about exp, sin, cos
2015-03-18 paulson 2015-03-18 Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
2015-03-17 paulson 2015-03-17 Merge
2015-03-16 paulson 2015-03-16 The factorial function, "fact", now has type "nat => 'a"
2015-03-13 wenzelm 2015-03-13 removed junk;
2015-03-10 paulson 2015-03-10 renaming HOL/Fact.thy -> Binomial.thy
2015-03-09 paulson 2015-03-09 sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex