# HG changeset patch
# User paulson
# Date 961155179 -7200
# Node ID d54b2c41fe0e04f3672f6ba138a9e74d86433e9e
# Parent  67ca888af420bc6e8e26b9c1d2802c9d80aac1c8
new lemma real_minus_diff_eq

diff -r 67ca888af420 -r d54b2c41fe0e src/HOL/Real/RealOrd.ML
--- 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 ****)