src/HOL/Real.thy
changeset 67084 e138d96ed083
parent 67051 e7e54a0b9197
child 67226 ec32cdaab97b