(*  Title:	 Real/RealOrd.thy
    ID: 	 $Id: RealOrd.thy,v 1.2 1999/09/23 16:39:08 paulson Exp $
    Author:      Jacques D. Fleuriot and Lawrence C. Paulson
    Copyright:   1998  University of Cambridge
    Description: Type "real" is a linear order
*)

RealOrd = RealDef +

instance real :: order (real_le_refl,real_le_trans,real_le_anti_sym,real_less_le)
instance real :: linorder (real_le_linear)

constdefs
   rabs   :: real => real
   "rabs r      == if 0r<=r then r else -r" 

end