src/HOL/Library/Extended_Real.thy
changeset 62005 68db98c2cd97
parent 61976 3a27957ac658
child 62049 b0f941e207cf