src/HOL/Analysis/Elementary_Metric_Spaces.thy
changeset 77509 3bc49507bae5
parent 77490 2c86ea8961b5
child 78037 37894dff0111