1.1 --- a/src/HOL/Real/real_arith0.ML	Fri Oct 05 23:58:52 2001 +0200
     1.2 +++ b/src/HOL/Real/real_arith0.ML	Sat Oct 06 00:02:46 2001 +0200
     1.3 @@ -118,7 +118,7 @@
     1.4  qed "";
     1.5  
     1.6  Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
     1.7 -\     ==> # 6*a <= # 5*l+i";
     1.8 +\     ==> 6*a <= 5*l+i";
     1.9  by (fast_arith_tac 1);
    1.10  qed "";
    1.11  *)