# HG changeset patch
# User nipkow
# Date 1422635703 -3600
# Node ID b0ac740fc5104707f40cee14a2102f387543e893
# Parent  513300fa2d09e18e2d91a3600cc39a83f0acc5e9
canonical name

diff -r 513300fa2d09 -r b0ac740fc510 src/HOL/Divides.thy
--- 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)