author | nipkow |
Fri, 30 Jan 2015 17:35:03 +0100 | |
changeset 59473 | b0ac740fc510 |
parent 59472 | 513300fa2d09 |
child 59474 | 4475b1a0141d |
--- a/src/HOL/Divides.thy Thu Jan 29 17:07:49 2015 +0100 +++ b/src/HOL/Divides.thy Fri Jan 30 17:35:03 2015 +0100 @@ -511,7 +511,7 @@ apply simp done -lemma div_minus[simp]: +lemma div_diff[simp]: "\<lbrakk> z dvd x; z dvd y\<rbrakk> \<Longrightarrow> (x - y) div z = x div z - y div z" using div_add[where y = "- z" for z] by (simp add: dvd_neg_div)