src/HOL/Inequalities.thy
Mon, 30 Oct 2017 13:18:41 +0000 haftmann tuned some proofs and added some lemmas
Sun, 08 Oct 2017 22:28:20 +0200 haftmann avoid name clashes on interpretation of abstract locales
Mon, 17 Oct 2016 11:46:22 +0200 nipkow setsum -> sum
Mon, 19 Sep 2016 20:06:21 +0200 fleury left_distrib ~> distrib_right, right_distrib ~> distrib_left
Fri, 27 May 2016 20:23:55 +0200 wenzelm tuned proofs, to allow unfold_abs_def;
Wed, 17 Feb 2016 21:51:57 +0100 haftmann dropped various legacy fact bindings
Tue, 01 Dec 2015 14:09:10 +0000 paulson Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
Tue, 17 Nov 2015 12:32:08 +0000 paulson Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
Fri, 13 Nov 2015 12:27:13 +0000 paulson Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
Tue, 10 Nov 2015 14:18:41 +0000 paulson Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Fri, 01 May 2015 20:25:57 +0200 nipkow simplified statement and proof
Tue, 28 Apr 2015 16:23:38 +0100 paulson New material about complex transcendental functions (especially Ln, Arg) and polynomials
Mon, 16 Mar 2015 16:59:59 +0100 wenzelm proper headers;
Mon, 16 Mar 2015 14:52:34 +0100 hoelzl add inequalities (move from AFP/Amortized_Complexity)
less more (0) tip