src/HOL/RealDef.thy

 end
 
 
 subsection{*The Reals Form an Ordered Field*}
 
-instance real :: ordered_field
+instance real :: linordered_field
 proof
   fix x y z :: real
   show "x \<le> y ==> z + x \<le> z + y" by (rule real_add_left_mono)
   show "x < y ==> 0 < z ==> z * x < z * y" by (rule real_mult_less_mono2)
   show "\<bar>x\<bar> = (if x < 0 then -x else x)" by (simp only: real_abs_def)
   show "sgn x = (if x=0 then 0 else if 0<x then 1 else - 1)"
     by (simp only: real_sgn_def)
 qed
 
-instance real :: lordered_ab_group_add ..
+instance real :: lattice_ab_group_add ..
 
 text{*The function @{term real_of_preal} requires many proofs, but it seems
 to be essential for proving completeness of the reals from that of the
 positive reals.*}
 

 by simp
  
 lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
 by simp
 
-instance real :: lordered_ring
+instance real :: lattice_ring
 proof
   fix a::real
   show "abs a = sup a (-a)"
     by (auto simp add: real_abs_def sup_real_def)
 qed