src/HOL/Hyperreal/HRealAbs.thy
Sat, 30 Dec 2000 22:03:46 +0100 paulson separation of HOL-Hyperreal from HOL-Real
less more (0) tip