1.1 --- a/src/HOL/Integ/IntArith.thy	Mon Feb 16 15:24:03 2004 +0100
     1.2 +++ b/src/HOL/Integ/IntArith.thy	Tue Feb 17 10:41:59 2004 +0100
     1.3 @@ -429,6 +429,7 @@
     1.4  val zle_add1_eq_le = thm "zle_add1_eq_le";
     1.5  val nonneg_eq_int = thm "nonneg_eq_int";
     1.6  val abs_minus_one = thm "abs_minus_one";
     1.7 +val of_int_number_of_eq = thm"of_int_number_of_eq";
     1.8  val nat_eq_iff = thm "nat_eq_iff";
     1.9  val nat_eq_iff2 = thm "nat_eq_iff2";
    1.10  val nat_less_iff = thm "nat_less_iff";