src/HOL/Library/Extended_Nonnegative_Real.thy
changeset 67970 8c012a49293a
parent 67727 ce3e87a51488
child 68406 6beb45f6cf67