# 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 <" "\ 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