src/HOL/Library/Extended_Nonnegative_Real.thy
changeset 68384 4a3fc3420747
parent 67727 ce3e87a51488
child 68406 6beb45f6cf67