src/HOL/Inequalities.thy
24 months ago haftmann 2017-10-30 tuned some proofs and added some lemmas
2017-10-08 haftmann 2017-10-08 avoid name clashes on interpretation of abstract locales
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-05-27 wenzelm 2016-05-27 tuned proofs, to allow unfold_abs_def;
2016-02-17 haftmann 2016-02-17 dropped various legacy fact bindings
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-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-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-05-01 nipkow 2015-05-01 simplified statement and proof
2015-04-28 paulson 2015-04-28 New material about complex transcendental functions (especially Ln, Arg) and polynomials
2015-03-16 wenzelm 2015-03-16 proper headers;
2015-03-16 hoelzl 2015-03-16 add inequalities (move from AFP/Amortized_Complexity)