# HG changeset patch
# User nipkow
# Date 1139407979 -3600
# Node ID 8971c306b94f87cd05b0f267454d730f0553708e
# Parent  f24c416a48146f38a50776e443a2a2831bf6a099
made "dvd" on numbers executable by simp.

diff -r f24c416a4814 -r 8971c306b94f src/HOL/Integ/IntDiv.thy
--- a/src/HOL/Integ/IntDiv.thy	Wed Feb 08 14:39:00 2006 +0100
+++ b/src/HOL/Integ/IntDiv.thy	Wed Feb 08 15:12:59 2006 +0100
@@ -1047,6 +1047,8 @@
 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]
+
 lemma zdvd_0_right [iff]: "(m::int) dvd 0"
 by (simp add: dvd_def)
 
diff -r f24c416a4814 -r 8971c306b94f src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Wed Feb 08 14:39:00 2006 +0100
+++ b/src/HOL/Integ/NatBin.thy	Wed Feb 08 15:12:59 2006 +0100
@@ -194,6 +194,9 @@
 by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
 
 
+subsubsection{* Divisibility *}
+
+declare dvd_eq_mod_eq_0[of "number_of x" "number_of y", standard, simp]
 
 ML
 {*