src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
2016-01-08 hoelzl 2016-01-08 fix code generation for uniformity: uniformity is a non-computable pure data.
2016-01-08 hoelzl 2016-01-08 add uniform spaces
2015-12-30 wenzelm 2015-12-30 more symbols;
2015-12-29 wenzelm 2015-12-29 more symbols;
2015-12-09 paulson 2015-12-09 sorted out eventually_mono
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-06-10 wenzelm 2015-06-10 isabelle update_cartouches;
2015-03-23 haftmann 2015-03-23 explicit commutative additive inverse operation; more explicit focal point for commutative monoids with an inverse operation
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-04-11 nipkow 2014-04-11 made divide_pos_pos a simp rule
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-05-25 wenzelm 2013-05-25 syntax translations always depend on context;
2013-01-31 hoelzl 2013-01-31 remove unnecessary assumption from real_normed_vector
2013-01-14 hoelzl 2013-01-14 move eventually_Ball_finite to Limits
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-11-28 wenzelm 2012-11-28 eliminated slightly odd identifiers;
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-10-01 wenzelm 2012-10-01 report sort assignment of visible type variables;
2011-11-30 wenzelm 2011-11-30 prefer typedef without extra definition and alternative name; tuned proofs;
2011-09-03 huffman 2011-09-03 remove duplicate lemma finite_choice in favor of finite_set_choice
2011-08-31 huffman 2011-08-31 generalize lemma isCont_vec_nth
2011-08-31 huffman 2011-08-31 convert proof to Isar-style
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-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 remove duplicate lemma disjoint_iff
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 avoid warnings about duplicate rules
2011-08-10 huffman 2011-08-10 follow standard naming scheme for sgn_vec_def
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-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Lexicon;
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-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-05-04 huffman 2010-05-04 make (f -- a --> x) an abbreviation for (f ---> x) (at a)
2010-05-04 huffman 2010-05-04 make (X ----> L) an abbreviation for (X ---> L) sequentially
2010-04-29 huffman 2010-04-29 move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
2010-04-29 huffman 2010-04-29 remove redundant constants pastecart, fstcart, sndcart; users should prefer Pair, fst, snd instead
2010-02-27 wenzelm 2010-02-27 more precise syntax antiquotations;
2010-02-21 wenzelm 2010-02-21 binder notation for default print_mode -- to avoid strange output if "xsymbols" is not active;
2010-02-21 wenzelm 2010-02-21 tuned headers; tuned proofs;
2010-02-11 wenzelm 2010-02-11 modernized translations; formal markup of @{syntax_const} and @{const_syntax};
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-07 hoelzl 2010-01-07 added syntax translation to automatically add finite typeclass to index type of cartesian product type
2010-01-06 himmelma 2010-01-06 Made finite cartesian products finite
2009-11-16 hoelzl 2009-11-16 removed hassize predicate
2009-10-23 himmelma 2009-10-23 distinguished session for multivariate analysis