1.1 --- a/src/HOL/Real/RealOrd.ML	Fri Jun 16 13:28:26 2000 +0200
     1.2 +++ b/src/HOL/Real/RealOrd.ML	Fri Jun 16 13:32:59 2000 +0200
     1.3 @@ -61,6 +61,11 @@
     1.4  
     1.5  Addsimprocs [Real_Cancel.sum_conv, Real_Cancel.rel_conv];
     1.6  
     1.7 +Goal "- (z - y) = y - (z::real)";
     1.8 +by (Simp_tac 1);
     1.9 +qed "real_minus_diff_eq";
    1.10 +Addsimps [real_minus_diff_eq];
    1.11 +
    1.12  
    1.13  (**** Theorems about the ordering ****)
    1.14