src/HOL/Analysis/Metric_Arith.thy
changeset 78619 193a24f78b00
parent 76987 4c275405faae