src/HOL/Analysis/Ball_Volume.thy
changeset 71606 b3b0d87edd20
parent 70817 dd675800469d
child 71633 07bec530f02e