| changeset 36304 | 6984744e6b34 |
| parent 36301 | 72f4d079ebf8 |
| child 36348 | 89c54f51f55a |
--- a/src/HOL/Rings.thy Fri Apr 23 15:17:59 2010 +0200 +++ b/src/HOL/Rings.thy Fri Apr 23 15:17:59 2010 +0200 @@ -518,7 +518,7 @@ lemma divide_1 [simp]: "a / 1 = a" by (simp add: divide_inverse) -lemma times_divide_eq_right: "a * (b / c) = (a * b) / c" +lemma times_divide_eq_right [simp]: "a * (b / c) = (a * b) / c" by (simp add: divide_inverse mult_assoc) lemma minus_divide_left: "- (a / b) = (-a) / b"