src/HOL/Multivariate_Analysis/Euclidean_Space.thy
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-08-19 paulson 2015-08-19 New material and fixes related to the forthcoming Stone-Weierstrass development
2015-06-10 wenzelm 2015-06-10 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-06-28 haftmann 2014-06-28 fact consolidation
2013-12-16 immler 2013-12-16 additional lemmas
2013-12-16 immler 2013-12-16 ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
2013-09-26 huffman 2013-09-26 tuned proofs
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
2011-09-12 huffman 2011-09-12 move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy
2011-08-31 huffman 2011-08-31 move lemmas from Topology_Euclidean_Space to Euclidean_Space
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 replace some continuous_on lemmas with more general versions
2011-08-23 huffman 2011-08-23 declare euclidean_simps [simp] at the point they are proved; avoid duplicate rule warnings;
2011-08-18 huffman 2011-08-18 declare euclidean_component_zero[simp] at the point it is proved
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-10 huffman 2011-08-10 split Linear_Algebra.thy from Euclidean_Space.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-09 huffman 2011-08-09 bounded_linear interpretation for euclidean_component
2011-07-24 haftmann 2011-07-24 adjusted to tailored version of bex_simps
2011-05-15 wenzelm 2011-05-15 simplified/unified method_setup/attribute_setup;
2011-03-14 hoelzl 2011-03-14 moved t2_spaces to HOL image
2011-03-13 wenzelm 2011-03-13 tuned headers;
2011-03-03 wenzelm 2011-03-03 tuned proofs -- eliminated prems;
2011-02-28 boehmes 2011-02-28 removed dependency on Dense_Linear_Order
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-11-28 nipkow 2010-11-28 gave more standard finite set rules simp and intro attribute
2010-11-22 hoelzl 2010-11-22 Replace surj by abbreviation; remove surj_on.
2010-11-05 hoelzl 2010-11-05 Extend convex analysis by Bogdan Grechuk
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-23 haftmann 2010-08-23 dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
2010-08-03 wenzelm 2010-08-03 tuned headers -- more precise load path;
2010-07-19 haftmann 2010-07-19 diff_minus subsumes diff_def
2010-07-07 hoelzl 2010-07-07 tuned
2010-07-05 huffman 2010-07-05 section -> subsection
2010-07-01 hoelzl 2010-07-01 Instantiate product type as euclidean space.
2010-06-30 huffman 2010-06-30 minimize dependencies on Numeral_Type
2010-06-30 huffman 2010-06-30 change type of 'dimension' to 'a itself => nat
2010-06-30 huffman 2010-06-30 generalize some euclidean_space lemmas
2010-06-28 haftmann 2010-06-28 inner_simps is not enough, need also local facts
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-05-09 huffman 2010-05-09 avoid using real-specific versions of generic lemmas
2010-05-04 huffman 2010-05-04 convert comments to 'text' blocks
2010-05-03 hoelzl 2010-05-03 Moved Convex theory to library.
2010-04-29 huffman 2010-04-29 generalize lemma adjoint_unique; simplify some proofs
2010-04-29 huffman 2010-04-29 fix latex url
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 unused function vector_power, unused lemma one_plus_of_nat_neq_0
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-04-28 huffman 2010-04-28 generalize LIMSEQ_vector to tendsto_vector
2010-04-28 huffman 2010-04-28 generalize orthogonal_clauses
2010-04-28 huffman 2010-04-28 remove redundant lemma vector_dist_norm
2010-04-28 huffman 2010-04-28 remove redundant lemma norm_0
2010-04-28 huffman 2010-04-28 generalize some euclidean space lemmas