# HG changeset patch
# User huffman
# Date 1228436889 28800
# Node ID 13d6f120992bfc3cbeb95bf45899dd242a03ad6b
# Parent  dc0ab579a5ca5c52a033327a5c8458cf13006000
revert to using eq_number_of_eq for simplification (Groebner_Examples.thy was broken)

diff -r dc0ab579a5ca -r 13d6f120992b src/HOL/Int.thy
--- 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