src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
2011-09-07 huffman 2011-09-07 avoid using legacy theorem names
2011-09-01 huffman 2011-09-01 modernize lemmas about 'continuous' and 'continuous_on'; improve automation of continuity proofs;
2011-08-31 huffman 2011-08-31 remove redundant lemma card_enum
2011-08-25 huffman 2011-08-25 replace some continuous_on lemmas with more general versions
2011-08-25 huffman 2011-08-25 generalize lemma finite_imp_compact_convex_hull and related lemmas
2011-08-25 huffman 2011-08-25 generalize some lemmas
2011-08-25 huffman 2011-08-25 generalize lemma convex_cone_hull
2011-08-25 huffman 2011-08-25 rename subset_{interior,closure} to {interior,closure}_mono; remove some legacy theorem names;
2011-08-25 huffman 2011-08-25 simplify definition of 'interior'; add lemmas interiorI and interiorE; change lemmas interior_unique and closure_unique to rule_format; tidy some proofs;
2011-08-24 huffman 2011-08-24 change some subsection headings to subsubsection
2011-08-23 huffman 2011-08-23 remove unnecessary lemma card_ge1
2011-08-23 huffman 2011-08-23 move connected_real_lemma to the one place it is used
2011-08-23 huffman 2011-08-23 declare euclidean_simps [simp] at the point they are proved; avoid duplicate rule warnings;
2011-08-21 huffman 2011-08-21 add lemmas interior_Times and closure_Times
2011-08-21 huffman 2011-08-21 remove unnecessary euclidean_space class constraints
2011-08-20 huffman 2011-08-20 remove redundant lemma real_0_le_divide_iff in favor or zero_le_divide_iff
2011-08-18 huffman 2011-08-18 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
2011-08-12 huffman 2011-08-12 make Multivariate_Analysis work with separate set type
2011-08-10 huffman 2011-08-10 avoid warnings about duplicate rules
2011-08-10 huffman 2011-08-10 full import paths
2011-08-09 huffman 2011-08-09 mark some redundant theorems as legacy
2011-07-30 haftmann 2011-07-30 tuned proofs
2011-07-25 haftmann 2011-07-25 adjusted to tailored version of ball_simps
2011-03-13 wenzelm 2011-03-13 tuned headers;
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-12-03 hoelzl 2010-12-03 adapt proofs to changed set_plus_image (cf. ee8d0548c148);
2010-12-02 hoelzl 2010-12-02 Prove rel_interior_convex_hull_union (by Grechuck Bogdan).
2010-11-26 wenzelm 2010-11-26 keep private things private, without comments;
2010-11-05 hoelzl 2010-11-05 Extend convex analysis by Bogdan Grechuk
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-08-23 haftmann 2010-08-23 dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
2010-07-05 huffman 2010-07-05 generalize type of is_interval to class euclidean_space
2010-07-01 huffman 2010-07-01 generalize more lemmas from ordered_euclidean_space to euclidean_space
2010-06-30 huffman 2010-06-30 minimize dependencies on Numeral_Type
2010-06-21 hoelzl 2010-06-21 Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
2010-05-11 hoelzl 2010-05-11 Removed usage of normalizating locales.
2010-05-09 huffman 2010-05-09 avoid using real-specific versions of generic lemmas
2010-05-07 haftmann 2010-05-07 prefix normalizing replaces class_semiring
2010-05-06 haftmann 2010-05-06 former free-floating field_comp_conv now in structure Normalizer
2010-05-03 huffman 2010-05-03 merged
2010-05-01 huffman 2010-05-01 move setsum lemmas to Product_plus.thy
2010-05-03 hoelzl 2010-05-03 Moved Convex theory to library.
2010-04-29 huffman 2010-04-29 remove redundant constants pastecart, fstcart, sndcart; users should prefer Pair, fst, snd instead
2010-04-28 huffman 2010-04-28 remove redundant lemma norm_0
2010-04-28 huffman 2010-04-28 move path-related stuff into new theory file
2010-04-27 huffman 2010-04-27 generalize types of path operations
2010-04-26 huffman 2010-04-26 move definitions and theorems for type real^1 to separate theory file
2010-04-26 huffman 2010-04-26 merged
2010-04-26 huffman 2010-04-26 fix lots of looping simp calls and other warnings
2010-04-26 haftmann 2010-04-26 dropped group_simps, ring_simps, field_eq_simps
2010-04-25 huffman 2010-04-25 generalize more constants and lemmas
2010-04-25 huffman 2010-04-25 simplify types of path operations (use real instead of real^1)
2010-04-25 huffman 2010-04-25 add lemmas convex_real_interval and convex_box
2010-04-24 huffman 2010-04-24 generalize more constants and lemmas
2010-04-24 huffman 2010-04-24 generalize constant closest_point
2010-04-01 nipkow 2010-04-01 tuned many proofs a bit
2010-03-04 hoelzl 2010-03-04 Generalized setsum_cases
2010-03-02 himmelma 2010-03-02 replaced \<bullet> with inner
2010-01-25 hoelzl 2010-01-25 Replaced vec1 and dest_vec1 by abbreviation.