src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
2013-01-14 hoelzl 2013-01-14 move prod instantiation of second_countable_topology to its definition
2013-01-14 hoelzl 2013-01-14 renamed countable_basis_space to second_countable_topology
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-12-03 hoelzl 2012-12-03 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
2012-11-27 immler 2012-11-27 based countable topological basis on Countable_Set
2012-11-16 hoelzl 2012-11-16 moved (b)choice_iff(') to Hilbert_Choice
2012-11-16 hoelzl 2012-11-16 move theorems to be more generally useable
2012-11-16 immler 2012-11-16 allow arbitrary enumerations of basis in locale for generation of borel sets
2012-11-15 immler 2012-11-15 regularity of measures, therefore: characterization of closure with infimum distance; characterize of compact sets as totally bounded; added Diagonal_Subsequence to Library; introduced (enumerable) topological basis; rational boxes as basis of ordered euclidean space; moved some lemmas upwards
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-10-05 wenzelm 2012-10-05 tuned proofs;
2012-06-25 wenzelm 2012-06-25 tuned proofs -- prefer direct "rotated" instead of old-style COMP;
2012-05-31 huffman 2012-05-31 remove stray reference to no-longer-existing theorem 'add'
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-03-12 noschinl 2012-03-12 use eventually_elim method
2011-12-05 huffman 2011-12-05 remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
2011-11-17 huffman 2011-11-17 Groups.thy: generalize several lemmas from class ab_group_add to class group_add
2011-10-27 huffman 2011-10-27 fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left
2011-09-22 huffman 2011-09-22 discontinued legacy theorem names from RealDef.thy
2011-09-20 huffman 2011-09-20 add lemmas within_empty and tendsto_bot; declare within_UNIV [simp]; tuned some proofs;
2011-09-12 huffman 2011-09-12 shorten proof of frontier_straddle
2011-09-12 huffman 2011-09-12 remove redundant lemma Lim_sequentially in favor of lemma LIMSEQ_def
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