src/HOL/Real.thy
changeset 66252 b73f94b366b7
parent 66155 2463cba9f18f
child 66515 85c505c98332