[isabelle-dev] HOL vs. HOL-Complex

Lawrence Paulson 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 mailing list