src/HOL/Library/Extended_Nonnegative_Real.thy
changeset 70490 c42a0a0a9a8d
parent 70381 b151d1f00204
child 71834 919a55257e62
equal deleted inserted replaced
70489:12d1e6e2c1d0 70490:c42a0a0a9a8d