src/HOL/Analysis/Metric_Arith.thy
changeset 80791 f38e59e1c019
parent 76987 4c275405faae