src/HOL/Library/Extended_Real.thy
changeset 51618 a3577cd80c41
parent 51351 dd1dd470690b
child 51774 916271d52466