src/HOL/Real.thy
changeset 65908 aefdb9e664c9
parent 65885 77d922eff5ac
child 66155 2463cba9f18f