equal
deleted
inserted
replaced
192 (if neg (number_of v' :: int) then Suc 0 |
192 (if neg (number_of v' :: int) then Suc 0 |
193 else nat (1 mod number_of v'))" |
193 else nat (1 mod number_of v'))" |
194 by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) |
194 by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) |
195 |
195 |
196 |
196 |
|
197 subsubsection{* Divisibility *} |
|
198 |
|
199 declare dvd_eq_mod_eq_0[of "number_of x" "number_of y", standard, simp] |
197 |
200 |
198 ML |
201 ML |
199 {* |
202 {* |
200 val nat_number_of_def = thm"nat_number_of_def"; |
203 val nat_number_of_def = thm"nat_number_of_def"; |
201 |
204 |