# HG changeset patch
# User paulson
# Date 961155219 -7200
# Node ID 8a15c357777053ed318a1655210e3ab40fbcd160
# Parent  d54b2c41fe0e04f3672f6ba138a9e74d86433e9e
uncommented the last 2 examples; tidied

diff -r d54b2c41fe0e -r 8a15c3577770 src/HOL/Real/ex/BinEx.ML
--- a/src/HOL/Real/ex/BinEx.ML	Fri Jun 16 13:32:59 2000 +0200
+++ b/src/HOL/Real/ex/BinEx.ML	Fri Jun 16 13:33:39 2000 +0200
@@ -326,12 +326,10 @@
 Goal "!!a::real. [| a <= b; b+b <= c |] ==> a+a <= c";
 by (fast_arith_tac 1);
 
-Goal "!!a::real. [| a+b <= i+j; a<=b; i<=j |] \
-\     ==> a+a <= j+j";
+Goal "!!a::real. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j";
 by (fast_arith_tac 1);
 
-Goal "!!a::real. [| a+b < i+j; a<b; i<j |] \
-\     ==> a+a < j+j";
+Goal "!!a::real. [| a+b < i+j; a<b; i<j |] ==> a+a < j+j";
 by (fast_arith_tac 1);
 
 Goal "!!a::real. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
@@ -345,7 +343,6 @@
 \     ==> a+a+a+a <= l+l+l+l";
 by (fast_arith_tac 1);
 
-(* Too slow. Needs "combine_coefficients" simproc
 Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
 \     ==> a+a+a+a+a <= l+l+l+l+i";
 by (fast_arith_tac 1);
@@ -353,5 +350,4 @@
 Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
 \     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
 by (fast_arith_tac 1);
-*)