1.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Sun Jan 18 13:58:17 2009 +0100
     1.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Wed Jan 28 16:29:16 2009 +0100
     1.3 @@ -224,10 +224,6 @@
     1.4    {* Method.no_args (Method.SIMPLE_METHOD' (full_simp_tac ring_ss)) *}
     1.5    {* computes distributive normal form in rings *}
     1.6  
     1.7 -lemmas ring_simps =
     1.8 -  l_zero r_zero l_neg r_neg minus_minus minus0
     1.9 -  l_one r_one l_null r_null l_minus r_minus
    1.10 -
    1.11  
    1.12  subsection {* Rings and the summation operator *}
    1.13