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