src/HOL/Real/RealDef.thy
changeset 14398 c5c47703f763
parent 14387 e96d5c42c4b0
child 14421 ee97b6463cb4
     1.1 --- a/src/HOL/Real/RealDef.thy	Thu Feb 19 10:41:32 2004 +0100
     1.2 +++ b/src/HOL/Real/RealDef.thy	Thu Feb 19 15:57:34 2004 +0100
     1.3 @@ -467,7 +467,6 @@
     1.4  apply (rule eq_Abs_REAL [of z])
     1.5  apply (rule eq_Abs_REAL [of w]) 
     1.6  apply (auto simp add: real_le real_zero_def preal_add_ac preal_cancels)
     1.7 -apply (cut_tac x="x+ya" and y="xa+y" in linorder_linear, auto) 
     1.8  done
     1.9  
    1.10