src/HOL/Analysis/Ball_Volume.thy
changeset 70900 954e7f79c25a
parent 70817 dd675800469d
child 71633 07bec530f02e