[isabelle-dev] construction of the real numbers

[Brian Huffman]

On Mon, May 10, 2010 at 12:41 AM, Walther Neuper <neuper at ist.tugraz.at> wrote:
> A comment you ask for: Your assumption, that "users should not need to know
> or care which construction of reals we use", does not apply in education.
>
> There are several attempts to design educational software for ("pure" and
> "applied") mathematics, which is _transparent_ in the sense, that the
> learner can access any knowledge underlying a particular calculation.

Hi Walther,

I completely agree with your comments. I guess I really meant to
distinguish the "users" of Isabelle theories from "readers" or
"students" of those theories. It is for the benefit of this second
group that the theory of Dedekind real numbers should be kept
available. I have personally learned a lot of new mathematics by
studying formalizations in Isabelle, and I hope that later students
will benefit by having two alternative constructions of the real
numbers to study.

- Brian