src/HOL/Analysis/Elementary_Normed_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 nipkow 2019-01-28 more canonical and less specialized syntax
4 months ago paulson 2019-01-22 renamings and new material
5 months ago haftmann 2019-01-14 tuned proofs
5 months ago immler 2019-01-07 reduced dependencies of Connected.thy
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