src/HOL/Real.thy
changeset 66495 0b46bd081228
parent 66155 2463cba9f18f
child 66515 85c505c98332
equal deleted inserted replaced
66487:307c19f24d5c 66495:0b46bd081228