src/HOL/Library/Extended_Real.thy
changeset 59154 68ca25931dce
parent 59115 f65ac77f7e07
child 59425 c5e79df8cc21