# HG changeset patch
# User paulson
# Date 1139483679 -3600
# Node ID 4301eb0f051fdde3a9d098c4e03dfa604f6e2060
# Parent  075550af9e11f481cd866a87cf8366d2fe565001
names for simprules

diff -r 075550af9e11 -r 4301eb0f051f src/HOL/Integ/IntDiv.thy
--- 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)
diff -r 075550af9e11 -r 4301eb0f051f src/HOL/Integ/NatBin.thy
--- 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
 {*