--- a/src/HOL/Analysis/Polytope.thy Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Analysis/Polytope.thy Sun Oct 16 09:31:04 2016 +0200
@@ -2603,7 +2603,7 @@
by (meson \<open>0 < a\<close> divide_less_eq floor_unique_iff)
have "?n * a \<le> a + x"
apply (simp add: algebra_simps)
- by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_divide_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
+ by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_div_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
also have "... < y"
by (rule 1)
finally have "?n * a < y" .
@@ -2616,7 +2616,7 @@
by (meson \<open>0 < a\<close> divide_less_eq floor_unique_iff)
have "?n * a \<le> a + y"
apply (simp add: algebra_simps)
- by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_divide_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
+ by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_div_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
also have "... < x"
by (rule 2)
finally have "?n * a < x" .