Admin/de_overload.ML
2007-06-12 wenzelm 2007-06-12 De-overloaded operations for int and real.