src/HOL/Transcendental.thy
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
2015-03-07 wenzelm 2015-03-07 clarified Drule.gen_all: observe context more carefully;
2015-03-05 paulson 2015-03-05 The function frac. Various lemmas about limits, series, the exp function, etc.
2015-03-04 nipkow 2015-03-04 Removed the obsolete functions "natfloor" and "natceiling"
2014-11-12 immler 2014-11-12 added lemmas: convert between powr and log in comparisons, pull log out of addition/subtraction
2014-11-12 immler 2014-11-12 code equation for powr
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-30 haftmann 2014-10-30 more simp rules concerning dvd and even/odd
2014-10-21 haftmann 2014-10-21 turn even into an abbreviation
2014-10-20 hoelzl 2014-10-20 add tendsto_const and tendsto_ident_at as simp and intro rules
2014-10-20 haftmann 2014-10-20 augmented and tuned facts on even/odd and division
2014-10-19 haftmann 2014-10-19 prefer generic elimination rules for even/odd over specialized unfold rules for nat
2014-10-13 immler 2014-10-13 relaxed class constraints for exp
2014-09-21 haftmann 2014-09-21 explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
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