src/HOL/Library/Extended_Nonnegative_Real.thy
changeset 67560 0fa87bd86566
parent 67456 7895c159d7b1
child 67691 db202a00a29c