src/HOL/Library/Extended_Real.thy
changeset 51387 dbc4a77488b2
parent 51351 dd1dd470690b
child 51774 916271d52466