src/HOL/Library/Extended_Nonnegative_Real.thy
changeset 70720 99e24569cc1f
parent 70381 b151d1f00204
child 71834 919a55257e62
equal deleted inserted replaced
70709:a95446297373 70720:99e24569cc1f