src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
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
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