src/HOL/Library/Extended_Nonnegative_Real.thy
changeset 82775 61c39a9e5415
parent 81804 5a2e05eb7001