| changeset 18978 | 8971c306b94f |
| parent 18708 | 4b3dadb4fe33 |
| child 18984 | 4301eb0f051f |
--- 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 {*