src/HOL/Real.thy
changeset 77830 0f2baf04b782
parent 77490 2c86ea8961b5
child 77934 01c88cf514fc