[isabelle-dev] construction of the real numbers

[Brian Huffman]

Hello all,

I recently finished a formalization of real numbers that uses Cauchy
sequences. I thought it might be good to replace the current
formalization (which uses Dedekind cuts) with this new one in time for
the upcoming Isabelle release.

Users should not need to know or care which construction of reals we
use. The primary advantage of the new formalization is its size: It is
shorter than the current development of the reals by about a thousand
lines of code. It reduces the size of the Isabelle/HOL heap image
(without proof objects) by almost a megabyte.

I would propose to move the current development of the reals into an
example theory, say HOL/ex/Dedekind_Real.thy.

Are there any objections or comments?

- Brian