src/HOL/Library/Extended_Nonnegative_Real.thy
changeset 62755 7fde2461f9ef
parent 62648 ee48e0b4f669
child 62975 1d066f6ab25d
equal deleted inserted replaced
62747:f65ef4723aca 62755:7fde2461f9ef