2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-09-13 huffman 2013-09-13 tuned proofs about 'convex'
2013-09-13 huffman 2013-09-13 generalized and simplified proofs of several theorems about convex sets
2013-09-12 huffman 2013-09-12 new lemmas
2013-04-09 hoelzl 2013-04-09 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
2012-09-27 wenzelm 2012-09-27 tuned proofs;
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-08-18 huffman 2011-08-18 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
2011-08-10 huffman 2011-08-10 avoid warnings about duplicate rules
2011-06-09 hoelzl 2011-06-09 lemma about differences of convex functions
2010-08-23 haftmann 2010-08-23 dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
2010-05-09 huffman 2010-05-09 avoid using real-specific versions of generic lemmas
2010-05-04 hoelzl 2010-05-04 Add Convex to Library build
2010-05-03 hoelzl 2010-05-03 Moved Convex theory to library.