src/HOL/Real/RealDef.thy
changeset 14398 c5c47703f763
parent 14387 e96d5c42c4b0
child 14421 ee97b6463cb4
--- 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