src/HOL/Real.thy
changeset 68585 1657b9a5dd5d
parent 68529 29235951f104
child 68662 227f85b1b98c