src/HOL/Library/Extended_Real.thy
changeset 59842 9fda99b3d5ee
parent 59679 2574977f9afa
child 60060 3630ecde4e7c