src/HOL/Library/Normalized_Fraction.thy
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