src/HOL/Library/Extended_Nonnegative_Real.thy
changeset 82637 c6c20afb29c2
parent 81804 5a2e05eb7001
child 82967 73af47bc277c