src/HOL/Library/Extended_Real.thy
changeset 51615 072a7249e1ac
parent 51351 dd1dd470690b
child 51774 916271d52466