src/HOL/Library/Extended_Nonnegative_Real.thy
changeset 81954 6f2bcdfa9a19
parent 81804 5a2e05eb7001
child 82967 73af47bc277c
equal deleted inserted replaced
81953:02d9844ff892 81954:6f2bcdfa9a19