src/HOL/Library/Extended_Nonnegative_Real.thy
changeset 64722 6df73de0d3c7
parent 64425 b17acc1834e3
child 65680 378a2f11bec9
equal deleted inserted replaced
64721:4b9c96c3850b 64722:6df73de0d3c7