--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Apr 29 14:20:26 2009 +0200
@@ -639,7 +639,7 @@
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)"
+ "\<lambda> x y. 1/2 * ((x::'a::{ordered_field,number_ring}) + y)"
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