src/HOL/Library/Extended_Real.thy
changeset 53296 65c60c782da5
parent 53216 ad2e09c30aa8
child 53374 a14d2a854c02