--- a/src/HOL/Int.thy Thu Dec 04 16:05:45 2008 -0800 +++ b/src/HOL/Int.thy Thu Dec 04 16:28:09 2008 -0800 @@ -1324,7 +1324,7 @@ lemmas rel_simps [simp] = less_number_of less_bin_simps le_number_of le_bin_simps - eq_number_of eq_bin_simps + eq_number_of_eq eq_bin_simps iszero_simps neg_simps