| changeset 18984 | 4301eb0f051f |
| parent 18978 | 8971c306b94f |
| child 19380 | b808efaa5828 |
--- 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 {*