diff -r b3b15305a1c9 -r c5c47703f763 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Thu Feb 19 10:41:32 2004 +0100
+++ b/src/HOL/Real/RealDef.thy	Thu Feb 19 15:57:34 2004 +0100
@@ -467,7 +467,6 @@
 apply (rule eq_Abs_REAL [of z])
 apply (rule eq_Abs_REAL [of w]) 
 apply (auto simp add: real_le real_zero_def preal_add_ac preal_cancels)
-apply (cut_tac x="x+ya" and y="xa+y" in linorder_linear, auto) 
 done