src/HOL/Real.thy
changeset 56547 e9bb73d7b6cf
parent 56536 aefb4a8da31f
child 56541 0e3abadbef39