changeset 64240 | eabf80376aab |
parent 63500 | 0dac030afd36 |
child 64591 | 240a39af9ec4 |
--- a/src/HOL/Library/Normalized_Fraction.thy Sun Oct 16 09:31:03 2016 +0200 +++ b/src/HOL/Library/Normalized_Fraction.thy Sun Oct 16 09:31:04 2016 +0200 @@ -10,7 +10,7 @@ apply (auto simp add: dvd_def) apply (subgoal_tac "-(y * k) = y * - k") apply (simp only:) -apply (erule nonzero_mult_divide_cancel_left) +apply (erule nonzero_mult_div_cancel_left) apply simp done