src/HOL/Analysis/Ball_Volume.thy
changeset 77011 3e48f8c6afc9
parent 74439 c278b1864592
equal deleted inserted replaced
77010:fead2b33acdc 77011:3e48f8c6afc9