src/HOL/Divides.thy
changeset 61944 5d06ecfdb472
parent 61799 4cf66f21b764
child 62390 842917225d56
     1.1 --- a/src/HOL/Divides.thy	Sun Dec 27 22:07:17 2015 +0100
     1.2 +++ b/src/HOL/Divides.thy	Mon Dec 28 01:26:34 2015 +0100
     1.3 @@ -2436,7 +2436,7 @@
     1.4    by (rule mod_int_unique [of a b q r],
     1.5      simp add: divmod_int_rel_def)
     1.6  
     1.7 -lemma abs_div: "(y::int) dvd x \<Longrightarrow> abs (x div y) = abs x div abs y"
     1.8 +lemma abs_div: "(y::int) dvd x \<Longrightarrow> \<bar>x div y\<bar> = \<bar>x\<bar> div \<bar>y\<bar>"
     1.9  by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
    1.10  
    1.11  text\<open>Suggested by Matthias Daum\<close>