| changeset 14390 | 55fe71faadda |
| parent 14387 | e96d5c42c4b0 |
| child 14436 | 77017c49c004 |
--- a/src/HOL/Integ/IntArith.thy Mon Feb 16 15:24:03 2004 +0100 +++ b/src/HOL/Integ/IntArith.thy Tue Feb 17 10:41:59 2004 +0100 @@ -429,6 +429,7 @@ val zle_add1_eq_le = thm "zle_add1_eq_le"; val nonneg_eq_int = thm "nonneg_eq_int"; val abs_minus_one = thm "abs_minus_one"; +val of_int_number_of_eq = thm"of_int_number_of_eq"; val nat_eq_iff = thm "nat_eq_iff"; val nat_eq_iff2 = thm "nat_eq_iff2"; val nat_less_iff = thm "nat_less_iff";