src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
2013-01-31 hoelzl 2013-01-31 simplify heine_borel type class
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-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-09-28 wenzelm 2012-09-28 tuned proofs;
2012-09-07 wenzelm 2012-09-07 tuned proofs;
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2011-09-20 huffman 2011-09-20 add lemmas within_empty and tendsto_bot; declare within_UNIV [simp]; tuned some proofs;
2011-09-12 huffman 2011-09-12 remove redundant lemma Lim_sequentially in favor of lemma LIMSEQ_def
2011-09-01 huffman 2011-09-01 modernize lemmas about 'continuous' and 'continuous_on'; improve automation of continuity proofs;
2011-08-28 huffman 2011-08-28 move class perfect_space into RealVector.thy; use not_open_singleton as perfect_space class axiom; generalize some lemmas to class perfect_space;
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 many proofs about subspace and span; reorder premises in rule span_induct;
2011-08-23 huffman 2011-08-23 declare euclidean_simps [simp] at the point they are proved; avoid duplicate rule warnings;
2011-08-22 huffman 2011-08-22 legacy theorem names
2011-08-21 huffman 2011-08-21 section -> subsection
2011-08-18 huffman 2011-08-18 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
2011-08-16 huffman 2011-08-16 add simp rules for isCont
2011-08-15 huffman 2011-08-15 generalize lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq to class topological_space
2011-08-15 huffman 2011-08-15 add lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq; simplify and generalize some proofs;
2011-08-15 huffman 2011-08-15 remove duplicate lemmas eventually_conjI, eventually_and, eventually_false
2011-08-12 huffman 2011-08-12 make Multivariate_Analysis work with separate set type
2011-08-11 huffman 2011-08-11 avoid duplicate rule warnings
2011-08-11 huffman 2011-08-11 modify euclidean_space class to include basis set
2011-08-11 huffman 2011-08-11 remove lemma stupid_ext
2011-08-10 huffman 2011-08-10 remove several redundant and unused theorems about derivatives
2011-08-10 huffman 2011-08-10 more uniform naming scheme for finite cartesian product type and related theorems
2011-08-10 huffman 2011-08-10 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
2011-08-10 huffman 2011-08-10 simplified definition of class euclidean_space; removed classes real_basis and real_basis_with_inner
2011-08-08 huffman 2011-08-08 fix perfect_space instance proof for finite cartesian product (cf. 5b970711fb39)
2011-07-28 hoelzl 2011-07-28 simplified definition of vector (also removed Cartesian_Euclidean_Space.from_nat which collides with Countable.from_nat)
2011-05-15 wenzelm 2011-05-15 simplified/unified method_setup/attribute_setup;
2010-11-28 nipkow 2010-11-28 gave more standard finite set rules simp and intro attribute
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 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-20 haftmann 2010-08-20 more concise characterization of of_nat operation and class semiring_char_0
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2010-07-01 hoelzl 2010-07-01 Add theory for indicator function.
2010-07-01 hoelzl 2010-07-01 Instantiate product type as euclidean space.
2010-06-23 hoelzl 2010-06-23 Make latex happy
2010-06-21 hoelzl 2010-06-21 Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.