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