src/HOL/Divides.thy
changeset 68644 242d298526a3
parent 68631 bc1369804692
child 69216 1a52baa70aed
     1.1 --- a/src/HOL/Divides.thy	Sun Jul 15 21:58:50 2018 +0100
     1.2 +++ b/src/HOL/Divides.thy	Mon Jul 16 23:33:28 2018 +0100
     1.3 @@ -607,7 +607,7 @@
     1.4    shows "a div b < 0"
     1.5  proof -
     1.6    have "a div b \<le> - 1 div b"
     1.7 -    using Divides.zdiv_mono1 assms by auto
     1.8 +    using zdiv_mono1 assms by auto
     1.9    also have "... \<le> -1"
    1.10      by (simp add: assms(2) div_eq_minus1)
    1.11    finally show ?thesis