src/HOL/Analysis/Metric_Arith.thy
changeset 78747 d03de7bc2137
parent 76987 4c275405faae