src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
 2011-08-11 huffman 2011-08-11 remove lemma stupid_ext file | diff | annotate 2011-08-10 huffman 2011-08-10 remove several redundant and unused theorems about derivatives file | diff | annotate 2011-08-10 huffman 2011-08-10 more uniform naming scheme for finite cartesian product type and related theorems file | diff | annotate 2011-08-10 huffman 2011-08-10 move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy file | diff | annotate 2011-08-10 huffman 2011-08-10 simplified definition of class euclidean_space; removed classes real_basis and real_basis_with_inner file | diff | annotate 2011-08-08 huffman 2011-08-08 fix perfect_space instance proof for finite cartesian product (cf. 5b970711fb39) file | diff | annotate 2011-07-28 hoelzl 2011-07-28 simplified definition of vector (also removed Cartesian_Euclidean_Space.from_nat which collides with Countable.from_nat) file | diff | annotate 2011-05-15 wenzelm 2011-05-15 simplified/unified method_setup/attribute_setup; file | diff | annotate 2010-11-28 nipkow 2010-11-28 gave more standard finite set rules simp and intro attribute file | diff | annotate 2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI file | diff | annotate 2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets file | diff | annotate 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. file | diff | annotate 2010-08-20 haftmann 2010-08-20 more concise characterization of of_nat operation and class semiring_char_0 file | diff | annotate 2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively file | diff | annotate 2010-07-01 hoelzl 2010-07-01 Add theory for indicator function. file | diff | annotate 2010-07-01 hoelzl 2010-07-01 Instantiate product type as euclidean space. file | diff | annotate 2010-06-23 hoelzl 2010-06-23 Make latex happy file | diff | annotate 2010-06-21 hoelzl 2010-06-21 Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class. file | diff | annotate