src/HOL/Analysis/metric_arith.ML
changeset 74245 282cd3aa6cc6
parent 74239 914a214e110e
child 74249 9d9e7ed01dbb