src/HOL/Library/Extended_Nonnegative_Real.thy
changeset 80784 3d9e7746d9db
parent 80777 623d46973cbe
child 81332 f94b30fa2b6c