[isabelle-dev] HOL vs. HOL-Complex
lp15 at cam.ac.uk
Wed Jul 2 18:14:41 CEST 2008
I see a giant misconception coming. The point of nonstandard analysis
is that it makes properties of limits, derivatives, and so forth much
easier to prove than can be done with the standard definitions. They
eliminate the necessity of arguments involving epsilon and delta. So
it would be a mistake to imagine that the nonstandard theories are
only useful for people who are exploring nonstandard analysis. They
should be valuable to anybody who wants to prove anything in analysis.
It would be a shame to see them buried somewhere.
More information about the isabelle-dev