src/HOL/Library/Extended_Real.thy
changeset 62005 68db98c2cd97
parent 61976 3a27957ac658
child 62049 b0f941e207cf
equal deleted inserted replaced
62004:8c6226d88ced 62005:68db98c2cd97