src/HOL/Library/Extended_Real.thy
changeset 59044 c04eccae1de8
parent 59023 4999a616336c
child 59115 f65ac77f7e07