src/HOL/Analysis/Abstract_Metric_Spaces.thy
changeset 79681 df1059ea8846
parent 78750 f229090cb8a3
child 80764 47c0aa388621
equal deleted inserted replaced
79680:0b58e85906a1 79681:df1059ea8846