src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
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.
2010-01-10 berghofe 2010-01-10 Adapted to changes in induct method.
2010-01-07 hoelzl 2010-01-07 finite annotation on cartesian product is now implicit.
2010-01-06 himmelma 2010-01-06 Made finite cartesian products finite
2009-12-11 haftmann 2009-12-11 avoid dependency on implicit dest rule predicate1D in proofs
2009-11-19 hoelzl 2009-11-19 Renamed vector_less_eq_def to the more usual name vector_le_def.
2009-11-16 hoelzl 2009-11-16 removed hassize predicate
2009-11-16 hoelzl 2009-11-16 Added new lemmas to Euclidean Space by Robert Himmelmann
2009-10-27 paulson 2009-10-27 merged
2009-10-23 himmelma 2009-10-23 distinguished session for multivariate analysis