src/HOL/Library/Extended_Nonnegative_Real.thy
changeset 68343 2941e58318c7
parent 67727 ce3e87a51488
child 68406 6beb45f6cf67