(*  Title       : HRealAbs.thy
    Author      : Jacques D. Fleuriot
    Copyright   : 1998  University of Cambridge
    Description : Absolute value function for the hyperreals
*) 

HRealAbs = HyperDef + RealAbs + 

constdefs
   hrabs   :: hypreal => hypreal
   "hrabs r      == if 0hr<=r then r else -r" 

end