src/HOL/Library/Extended_Real.thy
changeset 51548 757fa47af981
parent 51351 dd1dd470690b
child 51774 916271d52466