src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
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
2010-04-27 huffman 2010-04-27 generalize more continuity lemmas
2010-04-27 huffman 2010-04-27 generalized many lemmas about continuity
2010-04-26 huffman 2010-04-26 simplify definition of continuous_on; generalize some lemmas
2010-04-26 huffman 2010-04-26 move intervals section heading
2010-04-26 huffman 2010-04-26 remove unused, redundant constant inv_on
2010-04-26 huffman 2010-04-26 reorganize subsection headings
2010-04-26 huffman 2010-04-26 move definitions and theorems for type real^1 to separate theory file
2010-04-26 huffman 2010-04-26 merged
2010-04-26 huffman 2010-04-26 fix lots of looping simp calls and other warnings
2010-04-25 huffman 2010-04-25 define finer-than ordering on net type; move some theorems into Limits.thy