src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
2011-09-12 huffman 2011-09-12 remove trivial lemma Lim_at_iff_LIM
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-09-02 huffman 2011-09-02 simplify proof of Rats_dense_in_real; remove lemma Rats_dense_in_nn_real;
2011-09-01 huffman 2011-09-01 simplify some proofs about uniform continuity, and add some new ones; rename some theorems according to standard naming scheme;
2011-09-01 huffman 2011-09-01 modernize lemmas about 'continuous' and 'continuous_on'; improve automation of continuity proofs;
2011-08-31 huffman 2011-08-31 simplify/generalize some proofs
2011-08-31 huffman 2011-08-31 move lemmas from Topology_Euclidean_Space to Euclidean_Space
2011-08-29 huffman 2011-08-29 simplify some proofs
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-28 huffman 2011-08-28 discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
2011-08-26 huffman 2011-08-26 generalize and simplify proof of continuous_within_sequentially
2011-08-25 huffman 2011-08-25 replace some continuous_on lemmas with more general versions
2011-08-25 huffman 2011-08-25 remove legacy theorem Lim_inner
2011-08-25 huffman 2011-08-25 rename subset_{interior,closure} to {interior,closure}_mono; remove some legacy theorem names;
2011-08-25 huffman 2011-08-25 simplify definition of 'interior'; add lemmas interiorI and interiorE; change lemmas interior_unique and closure_unique to rule_format; tidy some proofs;
2011-08-24 huffman 2011-08-24 add lemma closure_union; simplify some proofs;
2011-08-24 huffman 2011-08-24 minimize imports
2011-08-24 huffman 2011-08-24 move everything related to 'norm' method into new theory file Norm_Arith.thy
2011-08-23 huffman 2011-08-23 declare euclidean_simps [simp] at the point they are proved; avoid duplicate rule warnings;
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