equal
deleted
inserted
replaced
63 by (simp add: zmult_int) |
63 by (simp add: zmult_int) |
64 lemma [code]: "m div n = nat (int m div int n)" |
64 lemma [code]: "m div n = nat (int m div int n)" |
65 by (simp add: zdiv_int [symmetric]) |
65 by (simp add: zdiv_int [symmetric]) |
66 lemma [code]: "m mod n = nat (int m mod int n)" |
66 lemma [code]: "m mod n = nat (int m mod int n)" |
67 by (simp add: zmod_int [symmetric]) |
67 by (simp add: zmod_int [symmetric]) |
|
68 lemma [code]: "(m < n) = (int m < int n)" |
|
69 by simp |
68 |
70 |
69 subsection {* Preprocessors *} |
71 subsection {* Preprocessors *} |
70 |
72 |
71 text {* |
73 text {* |
72 In contrast to @{term "Suc n"}, the term @{term "n + (1::nat)"} is no longer |
74 In contrast to @{term "Suc n"}, the term @{term "n + (1::nat)"} is no longer |