src/HOL/Library/Extended_Nonnegative_Real.thy
changeset 64213 b265dd04d57d
parent 64008 17a20ca86d62
child 64267 b9a1486e79be