src/HOL/Library/Extended_Nonnegative_Real.thy
changeset 70443 a21a96eda033
parent 70381 b151d1f00204
child 71834 919a55257e62