src/HOL/Analysis/Metric_Arith.thy
changeset 78093 cec875dcc59e
parent 76987 4c275405faae