src/HOL/Library/Extended_Nonnegative_Real.thy
changeset 63711 e4843a8a8b18
parent 63540 f8652d0534fa
child 63882 018998c00003