src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
2015-05-28 paulson 2015-05-28 Convex hulls: theorems about interior, etc. And a few simple lemmas.
2015-05-26 paulson 2015-05-26 New material about paths, and some lemmas
2015-05-05 immler 2015-05-05 closures of intervals
2015-03-25 wenzelm 2015-03-25 prefer local fixes;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-10-24 hoelzl 2014-10-24 use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
2014-08-05 wenzelm 2014-08-05 tuned proofs -- fewer warnings;
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-30 hoelzl 2014-06-30 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-05-07 hoelzl 2014-05-07 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
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 field_simps: better support for negation and division, and power
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-04-02 hoelzl 2014-04-02 extend continuous_intros; remove continuous_on_intros and isCont_intros
2014-04-02 hoelzl 2014-04-02 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
2014-03-18 huffman 2014-03-18 remove unnecessary finiteness assumptions from lemmas about setsum
2014-03-18 immler 2014-03-18 removed dependencies on theory Ordered_Euclidean_Space
2014-03-18 immler 2014-03-18 use cbox to relax class constraints
2014-03-15 haftmann 2014-03-15 more complete set of lemmas wrt. image and composition
2014-03-05 huffman 2014-03-05 remove lemmas in favor of more general ones: convex(_hull)_set_{plus,setsum}
2014-03-05 huffman 2014-03-05 generalize lemma closure_sum
2014-02-27 wenzelm 2014-02-27 more symbols;
2014-02-23 wenzelm 2014-02-23 tuned proofs;
2013-12-16 immler 2013-12-16 summarized notions related to ordered_euclidean_space and intervals in separate theory
2013-12-16 immler 2013-12-16 prefer box over greaterThanLessThan on euclidean_space
2013-11-17 wenzelm 2013-11-17 tuned proofs;
2013-11-05 hoelzl 2013-11-05 move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
2013-11-05 hoelzl 2013-11-05 use bdd_above and bdd_below for conditionally complete lattices
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 make 'linear' into a sublocale of 'bounded_linear'; replace 'linear_def' with 'linear_iff'
2013-09-04 wenzelm 2013-09-04 tuned proofs;
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-08-31 wenzelm 2013-08-31 tuned proofs;
2013-08-31 wenzelm 2013-08-31 tuned proofs;
2013-08-31 wenzelm 2013-08-31 tuned proofs;
2013-08-30 wenzelm 2013-08-30 tuned proofs;
2013-08-30 wenzelm 2013-08-30 tuned proofs;
2013-08-18 wenzelm 2013-08-18 more symbols;
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-03-26 hoelzl 2013-03-26 rename RealVector.thy to Real_Vector_Spaces.thy
2013-03-22 hoelzl 2013-03-22 move connected to HOL image; used to show intermediate value theorem
2013-03-22 hoelzl 2013-03-22 introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
2013-01-18 wenzelm 2013-01-18 merged
2013-01-18 wenzelm 2013-01-18 tuned proof -- much faster;
2013-01-18 hoelzl 2013-01-18 generalized diameter from real_normed_vector to metric_space
2013-01-10 wenzelm 2013-01-10 tuned proofs;
2012-12-14 hoelzl 2012-12-14 Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
2012-11-16 hoelzl 2012-11-16 move theorems to be more generally useable
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-09-22 wenzelm 2012-09-22 tuned whitespace;
2012-09-22 wenzelm 2012-09-22 tuned;
2012-09-22 wenzelm 2012-09-22 tuned proofs;
2012-04-12 krauss 2012-04-12 Set_Algebras: removed syntax \<oplus> and \<otimes>, in favour of plain + and *