| changeset 9081 | d54b2c41fe0e |
| parent 9069 | e8d530582061 |
| child 9434 | d2fa043ab24f |
--- 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 ****)