1.1 --- a/src/HOL/Real/RealDef.ML	Tue Nov 23 11:18:42 1999 +0100
     1.2 +++ b/src/HOL/Real/RealDef.ML	Tue Nov 23 11:19:39 1999 +0100
     1.3 @@ -461,6 +461,16 @@
     1.4  by (simp_tac (simpset() addsimps [real_mult_commute',real_add_mult_distrib]) 1);
     1.5  qed "real_add_mult_distrib2";
     1.6  
     1.7 +Goalw [real_diff_def] "((z1::real) - z2) * w = (z1 * w) - (z2 * w)";
     1.8 +by (simp_tac (simpset() addsimps [real_add_mult_distrib, 
     1.9 +				  real_minus_mult_eq1]) 1);
    1.10 +qed "real_diff_mult_distrib";
    1.11 +
    1.12 +Goal "(w::real) * (z1 - z2) = (w * z1) - (w * z2)";
    1.13 +by (simp_tac (simpset() addsimps [real_mult_commute', 
    1.14 +				  real_diff_mult_distrib]) 1);
    1.15 +qed "real_diff_mult_distrib2";
    1.16 +
    1.17  (*** one and zero are distinct ***)
    1.18  Goalw [real_zero_def,real_one_def] "0r ~= 1r";
    1.19  by (auto_tac (claset(),