# HG changeset patch
# User chaieb
# Date 1185119622 -7200
# Node ID 7392193f9ecf7db0bcfbba9a835ae90ecd6885cf
# Parent  b25b1444a24617bfec12f1e5a71576867ccc8b56
Tunes Proof

diff -r b25b1444a246 -r 7392193f9ecf src/HOL/Arith_Tools.thy
--- 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