src/HOL/Analysis/Elementary_Normed_Spaces.thy
Sat, 29 Dec 2018 20:32:09 +0100 immler split off theorems involving classes below metric_space and real_normed_vector
less more (0) tip