src/HOL/Real.thy
changeset 60306 6b7c64ab8bd2
parent 60162 645058aa9d6f
child 60352 d46de31a50c4