src/HOL/Library/Extended_Nonnegative_Real.thy
changeset 64818 67a0a563d2b3
parent 64425 b17acc1834e3
child 65680 378a2f11bec9