src/HOL/Analysis/Abstract_Metric_Spaces.thy
changeset 80771 fd01ef524169
parent 80764 47c0aa388621
child 80792 1cbdba868710