src/HOL/Analysis/Abstract_Metric_Spaces.thy
changeset 82313 df99e867c63e
parent 80792 1cbdba868710
equal deleted inserted replaced
82311:a3b556a23541 82313:df99e867c63e