src/HOL/Library/Convex.thy
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