# HG changeset patch
# User paulson
# Date 943352379 -3600
# Node ID 8a27d0579e37e21aab0d391ee993d9a0f2779015
# Parent  636884ec8f13d9f6efc12415b620210d0c67e9c5
distributive laws for * over -

diff -r 636884ec8f13 -r 8a27d0579e37 src/HOL/Real/RealDef.ML
--- a/src/HOL/Real/RealDef.ML	Tue Nov 23 11:18:42 1999 +0100
+++ b/src/HOL/Real/RealDef.ML	Tue Nov 23 11:19:39 1999 +0100
@@ -461,6 +461,16 @@
 by (simp_tac (simpset() addsimps [real_mult_commute',real_add_mult_distrib]) 1);
 qed "real_add_mult_distrib2";
 
+Goalw [real_diff_def] "((z1::real) - z2) * w = (z1 * w) - (z2 * w)";
+by (simp_tac (simpset() addsimps [real_add_mult_distrib, 
+				  real_minus_mult_eq1]) 1);
+qed "real_diff_mult_distrib";
+
+Goal "(w::real) * (z1 - z2) = (w * z1) - (w * z2)";
+by (simp_tac (simpset() addsimps [real_mult_commute', 
+				  real_diff_mult_distrib]) 1);
+qed "real_diff_mult_distrib2";
+
 (*** one and zero are distinct ***)
 Goalw [real_zero_def,real_one_def] "0r ~= 1r";
 by (auto_tac (claset(),