src/HOL/Transcendental.thy
2017-08-27 nipkow 2017-08-27 tuned
2017-08-26 nipkow 2017-08-26 reorganized and added log-related lemmas
2017-08-26 nipkow 2017-08-26 tuned proofs
2017-08-25 nipkow 2017-08-25 reorganization of tree lemmas; new lemmas
2017-08-22 Manuel Eberl 2017-08-22 Lemmas about analysis and permutations
2017-07-15 eberlm 2017-07-15 Simprocs for roots of numerals
2017-05-02 paulson 2017-05-02 Simplification of some proofs. Also key lemmas using !! rather than ! in premises
2017-04-26 paulson 2017-04-26 Further new material. The simprule status of some exp and ln identities was reverted.
2017-04-25 paulson 2017-04-25 New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
2017-04-22 wenzelm 2017-04-22 theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
2017-03-10 immler 2017-03-10 modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
2017-03-05 nipkow 2017-03-05 added numeral_powr_numeral
2017-02-27 paulson 2017-02-27 Some new lemmas thanks to Lukas Bulwahn. Also, NEWS.
2017-02-21 paulson 2017-02-21 Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion
2017-01-03 paulson 2017-01-03 A few new lemmas and needed adaptations
2016-11-22 nipkow 2016-11-22 added simp rule
2016-10-17 nipkow 2016-10-17 setprod -> prod
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-09-19 fleury 2016-09-19 left_distrib ~> distrib_right, right_distrib ~> distrib_left
2016-09-11 wenzelm 2016-09-11 tuned proofs;
2016-09-01 Manuel Eberl 2016-09-01 Some facts about factorial and binomial coefficients
2016-08-25 Manuel Eberl 2016-08-25 More analysis lemmas
2016-07-29 wenzelm 2016-07-29 more accurate cong del; tuned proofs;
2016-07-28 wenzelm 2016-07-28 misc tuning and modernization;
2016-07-22 wenzelm 2016-07-22 tuned proofs -- avoid unstructured calculation;
2016-07-12 wenzelm 2016-07-12 misc tuning and modernization;
2016-07-09 haftmann 2016-07-09 more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat * * * more rules for setsum, setprod on intervals
2016-07-02 haftmann 2016-07-02 simplified definitions of combinatorial functions
2016-07-02 haftmann 2016-07-02 more theorems
2016-06-13 eberlm 2016-06-13 Facts about HK integration, complex powers, Gamma function
2016-05-27 wenzelm 2016-05-27 tuned proofs, to allow unfold_abs_def;
2016-05-25 wenzelm 2016-05-25 isabelle update_cartouches -c -t;
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/...