[isabelle-dev] HOL vs. HOL-Complex

[Lawrence Paulson]

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.
Larry