src/HOL/Multivariate_Analysis/Path_Connected.thy
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-04-02 hoelzl 2014-04-02 extend continuous_intros; remove continuous_on_intros and isCont_intros
2014-03-18 immler 2014-03-18 use cbox to relax class constraints
2013-09-14 wenzelm 2013-09-14 tuned proofs;
2013-09-12 huffman 2013-09-12 removed outdated comments
2013-03-22 hoelzl 2013-03-22 move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
2013-03-22 hoelzl 2013-03-22 move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
2013-01-17 hoelzl 2013-01-17 generalize compact_path_image to topological_space
2013-01-14 hoelzl 2013-01-14 differentiate (cover) compactness and sequential compactness
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-09-28 wenzelm 2012-09-28 tuned proofs;
2012-09-28 wenzelm 2012-09-28 tuned proofs;
2012-06-25 wenzelm 2012-06-25 tuned proofs -- prefer direct "rotated" instead of old-style COMP;
2011-09-01 huffman 2011-09-01 modernize lemmas about 'continuous' and 'continuous_on'; improve automation of continuity proofs;
2011-08-25 huffman 2011-08-25 replace some continuous_on lemmas with more general versions
2011-08-12 huffman 2011-08-12 make Multivariate_Analysis work with separate set type
2011-03-13 wenzelm 2011-03-13 tuned headers;
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-07-01 huffman 2010-07-01 convert theorem path_connected_sphere to euclidean_space class
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-04-28 huffman 2010-04-28 move path-related stuff into new theory file