src/HOL/IntArith.thy

--- a/src/HOL/IntArith.thy	Tue Jul 31 19:26:35 2007 +0200
+++ b/src/HOL/IntArith.thy	Tue Jul 31 19:38:33 2007 +0200
@@ -14,10 +14,6 @@
   ("int_arith1.ML")
 begin
 
-text{*Duplicate: can't understand why it's necessary*}
-declare numeral_0_eq_0 [simp]
-
-
 subsection{*Inequality Reasoning for the Arithmetic Simproc*}
 
 lemma add_numeral_0: "Numeral0 + a = (a::'a::number_ring)"