new lemma real_minus_diff_eq

--- a/src/HOL/Real/RealOrd.ML	Fri Jun 16 13:28:26 2000 +0200
+++ b/src/HOL/Real/RealOrd.ML	Fri Jun 16 13:32:59 2000 +0200
@@ -61,6 +61,11 @@
 
 Addsimprocs [Real_Cancel.sum_conv, Real_Cancel.rel_conv];
 
+Goal "- (z - y) = y - (z::real)";
+by (Simp_tac 1);
+qed "real_minus_diff_eq";
+Addsimps [real_minus_diff_eq];
+
 
 (**** Theorems about the ordering ****)