1.1 --- a/src/HOL/Hyperreal/hypreal_arith0.ML	Fri Oct 05 21:50:37 2001 +0200
     1.2 +++ b/src/HOL/Hyperreal/hypreal_arith0.ML	Fri Oct 05 21:52:39 2001 +0200
     1.3 @@ -115,7 +115,7 @@
     1.4  qed "";
     1.5  
     1.6  Goal "!!a::hypreal. [| 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  *)