src/HOL/Real.thy
changeset 66117 e6f808d1307c
parent 65885 77d922eff5ac
child 66155 2463cba9f18f