src/HOL/Library/Convex.thy
2016-02-10 hoelzl 2016-02-10 Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
2015-11-17 paulson 2015-11-17 Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
2015-11-05 wenzelm 2015-11-05 isabelle update_cartouches -c -t;
2015-11-02 eberlm 2015-11-02 Rounding function, uniform limits, cotangent, binomial identities
2015-10-27 paulson 2015-10-27 Cauchy's integral formula, required lemmas, and a bit of reorganisation
2015-10-26 paulson 2015-10-26 new lemmas about topology, etc., for Cauchy integral formula
2015-10-13 paulson 2015-10-13 new material on path_component_sets, inside, outside, etc. And more default simprules
2015-08-31 wenzelm 2015-08-31 prefer symbols;
2015-06-13 wenzelm 2015-06-13 renamed "prems" to "that";
2015-06-10 wenzelm 2015-06-10 misc tuning;
2015-05-26 paulson 2015-05-26 New material about paths, and some lemmas
2015-05-05 immler 2015-05-05 generalized differentiable_bound; some further variations of differentiable_bound
2015-03-31 paulson 2015-03-31 New material and binomial fix
2015-02-19 haftmann 2015-02-19 establish unique preferred fact names
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-04-29 wenzelm 2014-04-29 tuned proofs;
2014-04-14 hoelzl 2014-04-14 added divide_nonneg_nonneg and co; made it a simp rule
2014-04-12 nipkow 2014-04-12 made mult_pos_pos a simp rule
2014-04-11 nipkow 2014-04-11 made divide_pos_pos a simp rule
2014-04-11 nipkow 2014-04-11 made mult_nonneg_nonneg a simp rule
2014-04-09 hoelzl 2014-04-09 revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
2014-04-03 paulson 2014-04-03 removing simprule status for divide_minus_left and divide_minus_right
2014-03-04 huffman 2014-03-04 tuned proof script
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.