src/HOL/Real.thy
changeset 68586 006da53a8ac1
parent 68529 29235951f104
child 68662 227f85b1b98c