[isabelle-dev] construction of the real numbers

[Tobias Nipkow]

That sounds very worthwhile, thanks!

Tobias

Brian Huffman wrote:
> 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
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev