src/HOL/ex/BinEx.thy

--- a/src/HOL/ex/BinEx.thy	Thu Feb 19 10:41:32 2004 +0100
+++ b/src/HOL/ex/BinEx.thy	Thu Feb 19 15:57:34 2004 +0100
@@ -471,7 +471,6 @@
   apply (simp add: normal_Pls_eq_0)
   apply (simp only: number_of_minus zminus_0 iszero_def
                     minus_equation_iff [of _ "0"])
-  apply (simp add: eq_commute)
   done
 
 (*The previous command should have finished the proof but the lin-arith