src/HOL/Arith_Tools.thy
changeset 23901 7392193f9ecf
parent 23881 851c74f1bb69
child 24075 366d4d234814
--- a/src/HOL/Arith_Tools.thy	Sun Jul 22 13:53:52 2007 +0200
+++ b/src/HOL/Arith_Tools.thy	Sun Jul 22 17:53:42 2007 +0200
@@ -697,12 +697,10 @@
   using eq_diff_eq[where a= x and b=t and c=0] by simp
 
 
-interpretation class_ordered_field_dense_linear_order: dense_linear_order
+interpretation class_ordered_field_dense_linear_order: constr_dense_linear_order
  ["op <=" "op <"
    "\<lambda> x y. 1/2 * ((x::'a::{ordered_field,recpower,number_ring}) + y)"]
-proof (unfold_locales,
-  simp_all only: ordered_field_no_ub ordered_field_no_lb,
-    auto simp add: linorder_not_le)
+proof (unfold_locales, dlo, dlo, auto)
   fix x y::'a assume lt: "x < y"
   from  less_half_sum[OF lt] show "x < (x + y) /2" by simp
 next