made "dvd" on numbers executable by simp.

--- 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)
 

--- 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
 {*