--- a/src/HOL/Integ/IntDiv.thy Thu Feb 09 03:34:56 2006 +0100
+++ b/src/HOL/Integ/IntDiv.thy Thu Feb 09 12:14:39 2006 +0100
@@ -1047,7 +1047,10 @@
lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
by(simp add:dvd_def zmod_eq_0_iff)
-declare zdvd_iff_zmod_eq_0[of "number_of x" "number_of y", standard, simp]
+lemmas zdvd_iff_zmod_eq_0_number_of =
+ zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard]
+
+declare zdvd_iff_zmod_eq_0_number_of [simp]
lemma zdvd_0_right [iff]: "(m::int) dvd 0"
by (simp add: dvd_def)
--- a/src/HOL/Integ/NatBin.thy Thu Feb 09 03:34:56 2006 +0100
+++ b/src/HOL/Integ/NatBin.thy Thu Feb 09 12:14:39 2006 +0100
@@ -196,7 +196,10 @@
subsubsection{* Divisibility *}
-declare dvd_eq_mod_eq_0[of "number_of x" "number_of y", standard, simp]
+lemmas dvd_eq_mod_eq_0_number_of =
+ dvd_eq_mod_eq_0 [of "number_of x" "number_of y", standard]
+
+declare dvd_eq_mod_eq_0_number_of [simp]
ML
{*