src/HOL/Real.thy
changeset 77537 1bbf29ec9ce3
parent 77490 2c86ea8961b5
child 77934 01c88cf514fc