| changeset 16295 | cd7a83dae4f9 |
| parent 15574 | b1d1b5bfc464 |
| child 16770 | 1f1b1fae30e4 |
--- a/src/HOL/Library/EfficientNat.thy Mon Jun 06 10:21:53 2005 +0200 +++ b/src/HOL/Library/EfficientNat.thy Mon Jun 06 11:30:57 2005 +0200 @@ -65,6 +65,8 @@ by (simp add: zdiv_int [symmetric]) lemma [code]: "m mod n = nat (int m mod int n)" by (simp add: zmod_int [symmetric]) +lemma [code]: "(m < n) = (int m < int n)" + by simp subsection {* Preprocessors *}