src/HOL/Real/Real.thy
changeset 5548 5cd3396802f5
parent 5078 7b5ea59c0275
child 5588 a3ab526bb891