src/HOL/Library/Convex.thy
Mon, 02 Nov 2015 11:56:28 +0100 eberlm Rounding function, uniform limits, cotangent, binomial identities
Tue, 27 Oct 2015 15:17:02 +0000 paulson Cauchy's integral formula, required lemmas, and a bit of reorganisation
Mon, 26 Oct 2015 23:41:27 +0000 paulson new lemmas about topology, etc., for Cauchy integral formula
Tue, 13 Oct 2015 12:42:08 +0100 paulson new material on path_component_sets, inside, outside, etc. And more default simprules
Mon, 31 Aug 2015 21:28:08 +0200 wenzelm prefer symbols;
Sat, 13 Jun 2015 13:09:05 +0200 wenzelm renamed "prems" to "that";
Wed, 10 Jun 2015 22:28:56 +0200 wenzelm misc tuning;
Tue, 26 May 2015 21:58:04 +0100 paulson New material about paths, and some lemmas
Tue, 05 May 2015 18:45:10 +0200 immler generalized differentiable_bound; some further variations of differentiable_bound
Tue, 31 Mar 2015 15:00:03 +0100 paulson New material and binomial fix
Thu, 19 Feb 2015 11:53:36 +0100 haftmann establish unique preferred fact names
Sun, 02 Nov 2014 17:20:45 +0100 wenzelm modernized header;
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
Sat, 28 Jun 2014 09:16:42 +0200 haftmann fact consolidation
Tue, 29 Apr 2014 22:50:55 +0200 wenzelm tuned proofs;
Mon, 14 Apr 2014 13:08:17 +0200 hoelzl added divide_nonneg_nonneg and co; made it a simp rule
Sat, 12 Apr 2014 17:26:27 +0200 nipkow made mult_pos_pos a simp rule
Fri, 11 Apr 2014 22:53:33 +0200 nipkow made divide_pos_pos a simp rule
Fri, 11 Apr 2014 13:36:57 +0200 nipkow made mult_nonneg_nonneg a simp rule
Wed, 09 Apr 2014 09:37:47 +0200 hoelzl revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
Thu, 03 Apr 2014 23:51:52 +0100 paulson removing simprule status for divide_minus_left and divide_minus_right
Tue, 04 Mar 2014 14:00:59 -0800 huffman tuned proof script
Fri, 01 Nov 2013 18:51:14 +0100 haftmann more simplification rules on unary and binary minus
Fri, 13 Sep 2013 14:57:20 -0700 huffman tuned proofs about 'convex'
Fri, 13 Sep 2013 11:16:13 -0700 huffman generalized and simplified proofs of several theorems about convex sets
Thu, 12 Sep 2013 09:33:36 -0700 huffman new lemmas
Tue, 09 Apr 2013 14:04:47 +0200 hoelzl move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
Thu, 27 Sep 2012 14:52:50 +0200 wenzelm tuned proofs;
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Thu, 18 Aug 2011 13:36:58 -0700 huffman remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
Wed, 10 Aug 2011 18:02:16 -0700 huffman avoid warnings about duplicate rules
Thu, 09 Jun 2011 11:50:16 +0200 hoelzl lemma about differences of convex functions
Mon, 23 Aug 2010 11:17:13 +0200 haftmann dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
Sun, 09 May 2010 22:51:11 -0700 huffman avoid using real-specific versions of generic lemmas
Tue, 04 May 2010 18:05:22 +0200 hoelzl Add Convex to Library build
Mon, 03 May 2010 14:35:10 +0200 hoelzl Moved Convex theory to library.
less more (0) tip