src/HOL/Library/Extended_Nonnegative_Real.thy
changeset 68446 92ddca1edc43
parent 68406 6beb45f6cf67
child 68527 2f4e2aab190a