On Mon, May 10, 2010 at 12:41 AM, Walther Neuper <[email protected]> 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 _______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
