1.1 --- a/src/HOL/Arith_Tools.thy	Sun Jul 22 13:53:52 2007 +0200
     1.2 +++ b/src/HOL/Arith_Tools.thy	Sun Jul 22 17:53:42 2007 +0200
     1.3 @@ -697,12 +697,10 @@
     1.4    using eq_diff_eq[where a= x and b=t and c=0] by simp
     1.5  
     1.6  
     1.7 -interpretation class_ordered_field_dense_linear_order: dense_linear_order
     1.8 +interpretation class_ordered_field_dense_linear_order: constr_dense_linear_order
     1.9   ["op <=" "op <"
    1.10     "\<lambda> x y. 1/2 * ((x::'a::{ordered_field,recpower,number_ring}) + y)"]
    1.11 -proof (unfold_locales,
    1.12 -  simp_all only: ordered_field_no_ub ordered_field_no_lb,
    1.13 -    auto simp add: linorder_not_le)
    1.14 +proof (unfold_locales, dlo, dlo, auto)
    1.15    fix x y::'a assume lt: "x < y"
    1.16    from  less_half_sum[OF lt] show "x < (x + y) /2" by simp
    1.17  next