src/HOL/Analysis/Elementary_Metric_Spaces.thy
5 weeks ago paulson 2019-03-19 new material about topology, etc.; also fixes for yesterday's
5 weeks ago paulson 2019-03-18 new material;' strengthened material; moved proofs out of Function_Topology in order to lessen its dependencies
3 months ago paulson 2019-01-22 renamings and new material
3 months ago immler 2019-01-16 chapters for analysis manual
3 months ago immler 2019-01-07 moved generalized lemmas
3 months ago immler 2019-01-07 generalized
3 months ago immler 2019-01-07 moved setdist to more appropriate places
3 months ago immler 2019-01-07 split off theory combining Elementary_Topology and Abstract_Topology
3 months ago immler 2019-01-07 moved material from Connected.thy to more appropriate places
3 months ago immler 2019-01-07 moved material from Connected.thy to more appropriate places
3 months ago immler 2019-01-06 moved some material from Connected.thy to more appropriate places
3 months ago immler 2018-12-29 split off theorems involving classes below metric_space and real_normed_vector