src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
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.