src/HOL/Library/Extended_Nonnegative_Real.thy
changeset 68423 c1db7503dbaa
parent 68406 6beb45f6cf67
child 68527 2f4e2aab190a