src/HOL/Library/Extended_Nonnegative_Real.thy
changeset 62379 340738057c8c
parent 62378 85ed00c1fe7c
child 62623 dbc62f86a1a9