src/HOL/Real/RealDef.thy
changeset 22456 6070e48ecb78
parent 21404 eb85850d3eb7
child 22958 b3a5569a81e5
     1.1 --- a/src/HOL/Real/RealDef.thy	Fri Mar 16 21:32:11 2007 +0100
     1.2 +++ b/src/HOL/Real/RealDef.thy	Fri Mar 16 21:32:12 2007 +0100
     1.3 @@ -434,6 +434,11 @@
     1.4  by (simp add: real_zero_def real_one_def real_le 
     1.5                   preal_self_less_add_left order_less_imp_le)
     1.6  
     1.7 +instance real :: distrib_lattice
     1.8 +  "inf x y \<equiv> min x y"
     1.9 +  "sup x y \<equiv> max x y"
    1.10 +  by default (auto simp add: inf_real_def sup_real_def min_max.sup_inf_distrib1)
    1.11 +
    1.12  
    1.13  subsection{*The Reals Form an Ordered Field*}
    1.14  
    1.15 @@ -446,8 +451,6 @@
    1.16      by (auto dest: order_le_less_trans simp add: real_abs_def linorder_not_le)
    1.17  qed
    1.18  
    1.19 -
    1.20 -
    1.21  text{*The function @{term real_of_preal} requires many proofs, but it seems
    1.22  to be essential for proving completeness of the reals from that of the
    1.23  positive reals.*}