src/HOL/Library/Extended_Nonnegative_Real.thy
changeset 68743 91162dd89571
parent 68527 2f4e2aab190a
child 68752 f221bc388ad0