src/HOL/Real.thy
changeset 67024 72d37a2e9cca
parent 66912 a99a7cbf0fb5
child 67051 e7e54a0b9197