src/HOL/Real.thy
changeset 64377 c1db9e3fe0e2
parent 64267 b9a1486e79be
child 65885 77d922eff5ac