src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
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-27 hoelzl 2010-08-27 preimages of open sets over continuous function are open
2010-08-23 hoelzl 2010-08-23 Rewrite the Probability theory. Introduced pinfreal as real numbers with infinity. Use pinfreal as value for measures. Introduces Lebesgue Measure based on the integral in Multivariate Analysis. Proved Radon Nikodym for arbitrary sigma finite measure spaces.
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-02 haftmann 2010-07-02 merged
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2010-07-01 huffman 2010-07-01 generalize more lemmas from ordered_euclidean_space to euclidean_space
2010-06-30 huffman 2010-06-30 add lemma at_within_interior
2010-06-22 hoelzl 2010-06-22 merged
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-06-21 blanchet 2010-06-21 beta-eta was too much, because it transformed SOME x. P x into Eps P, which caused problems later; reintroduced old proof based on Metis, since it was a good test for the Skolemizer
2010-06-17 haftmann 2010-06-17 replaced unreliable metis proof
2010-05-09 huffman 2010-05-09 avoid using real-specific versions of generic lemmas
2010-05-04 huffman 2010-05-04 generalize some lemmas to class t1_space
2010-05-04 huffman 2010-05-04 simplify definition of t1_space; generalize lemma closed_sing and related lemmas
2010-05-04 huffman 2010-05-04 generalize some lemmas
2010-05-04 huffman 2010-05-04 make (X ----> L) an abbreviation for (X ---> L) sequentially
2010-05-04 huffman 2010-05-04 adapt to removed premise on tendsto lemma (cf. 88f0125c3bd2)
2010-05-03 hoelzl 2010-05-03 Moved Convex theory to library.
2010-04-29 huffman 2010-04-29 define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
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 prove lemma openin_subopen without using choice
2010-04-27 huffman 2010-04-27 generalize more continuity lemmas
2010-04-27 huffman 2010-04-27 generalized many lemmas about continuity
2010-04-26 huffman 2010-04-26 simplify definition of continuous_on; generalize some lemmas
2010-04-26 huffman 2010-04-26 move intervals section heading
2010-04-26 huffman 2010-04-26 remove unused, redundant constant inv_on
2010-04-26 huffman 2010-04-26 reorganize subsection headings
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-25 huffman 2010-04-25 define finer-than ordering on net type; move some theorems into Limits.thy
2010-04-25 huffman 2010-04-25 generalize type of continuous_on
2010-04-25 huffman 2010-04-25 define nets directly as filters, instead of as filter bases
2010-04-26 haftmann 2010-04-26 dropped group_simps, ring_simps, field_eq_simps
2010-04-24 huffman 2010-04-24 minimize imports
2010-03-18 haftmann 2010-03-18 dropped odd interpretation of comm_monoid_mult into comm_monoid_add; consider Min.insert_idem as default simp rule
2010-02-17 himmelma 2010-02-17 Added integration to Multivariate-Analysis (upto FTC)
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-02-04 hoelzl 2010-02-04 Changed 'bounded unique existential quantifiers' from a constant to syntax translation.
2010-01-25 hoelzl 2010-01-25 Replaced vec1 and dest_vec1 by abbreviation.
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-11-23 huffman 2009-11-23 replace 'UNIV - S' with '- S'
2009-11-24 huffman 2009-11-24 re-state lemmas using 'range'
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-29 paulson 2009-10-29 Tidied up some very ugly proofs
2009-10-27 paulson 2009-10-27 merged
2009-10-23 himmelma 2009-10-23 distinguished session for multivariate analysis