src/HOL/Real.thy
changeset 54506 8b5caa190054
parent 54489 03ff4d1e6784
child 54863 82acc20ded73