src/HOL/Library/Extended_Real.thy
changeset 59370 b13ff987c559
parent 59115 f65ac77f7e07
child 59425 c5e79df8cc21