src/HOL/Analysis/metric_arith.ML
changeset 73594 5c4a09c4bc9c
parent 70962 e8207714d505
child 74239 914a214e110e