src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
2011-08-21 huffman 2011-08-21 add lemmas interior_Times and closure_Times
2011-08-20 huffman 2011-08-20 redefine constant 'trivial_limit' as an abbreviation
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-17 huffman 2011-08-17 Topology_Euclidean_Space.thy: simplify some proofs
2011-08-17 huffman 2011-08-17 simplify proofs of lemmas open_interval, closed_interval
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 generalized lemma closed_Collect_eq
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 generalize lemma continuous_uniform_limit to class metric_space
2011-08-15 huffman 2011-08-15 remove duplicate lemmas eventually_conjI, eventually_and, eventually_false
2011-08-15 huffman 2011-08-15 Topology_Euclidean_Space.thy: organize section headings
2011-08-14 huffman 2011-08-14 locale-ize some definitions, so perfect_space and heine_borel can inherit from the proper superclasses
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-10 huffman 2011-08-10 remove redundant lemma
2011-08-10 huffman 2011-08-10 simplify proof of lemma bounded_component
2011-08-10 huffman 2011-08-10 split Linear_Algebra.thy from Euclidean_Space.thy
2011-08-10 huffman 2011-08-10 declare tendsto_const [intro] (accidentally removed in 230a8665c919)
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-08-09 huffman 2011-08-09 mark some redundant theorems as legacy
2011-08-08 huffman 2011-08-08 instance real_basis_with_inner < perfect_space
2011-08-08 huffman 2011-08-08 rename type 'a net to 'a filter, following standard mathematical terminology
2011-08-08 huffman 2011-08-08 generalize sequence lemmas
2011-08-08 huffman 2011-08-08 generalize more lemmas about compactness
2011-08-08 huffman 2011-08-08 generalize compactness equivalence lemmas
2011-08-08 huffman 2011-08-08 lemma bolzano_weierstrass_imp_compact
2011-08-08 huffman 2011-08-08 class perfect_space inherits from topological_space; generalized several lemmas
2011-06-09 hoelzl 2011-06-09 lemmas about right derivative and limits
2011-03-30 hoelzl 2011-03-30 real multiplication is continuous
2011-03-14 hoelzl 2011-03-14 generalize infinite sums
2011-03-14 hoelzl 2011-03-14 moved t2_spaces to HOL image
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-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-27 hoelzl 2010-08-27 preimages of open sets over continuous function are open
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-07-05 huffman 2010-07-05 generalize type of is_interval to class euclidean_space
2010-07-02 haftmann 2010-07-02 merged
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2010-07-01 huffman 2010-07-01 generalize more lemmas from ordered_euclidean_space to euclidean_space
2010-06-30 huffman 2010-06-30 add lemma at_within_interior
2010-06-22 hoelzl 2010-06-22 merged
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-06-21 blanchet 2010-06-21 beta-eta was too much, because it transformed SOME x. P x into Eps P, which caused problems later; reintroduced old proof based on Metis, since it was a good test for the Skolemizer
2010-06-17 haftmann 2010-06-17 replaced unreliable metis proof
2010-05-09 huffman 2010-05-09 avoid using real-specific versions of generic lemmas
2010-05-04 huffman 2010-05-04 generalize some lemmas to class t1_space
2010-05-04 huffman 2010-05-04 simplify definition of t1_space; generalize lemma closed_sing and related lemmas
2010-05-04 huffman 2010-05-04 generalize some lemmas
2010-05-04 huffman 2010-05-04 make (X ----> L) an abbreviation for (X ---> L) sequentially
2010-05-04 huffman 2010-05-04 adapt to removed premise on tendsto lemma (cf. 88f0125c3bd2)
2010-05-03 hoelzl 2010-05-03 Moved Convex theory to library.
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 redundant constants pastecart, fstcart, sndcart; users should prefer Pair, fst, snd instead
2010-04-28 huffman 2010-04-28 prove lemma openin_subopen without using choice