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