src/HOL/Analysis/Ball_Volume.thy
changeset 80753 66893c47500d
parent 74439 c278b1864592
equal deleted inserted replaced
80752:2c9b5288eb84 80753:66893c47500d