1.1 --- a/src/HOL/Algebra/abstract/Ring.ML	Tue May 11 14:00:02 2004 +0200
     1.2 +++ b/src/HOL/Algebra/abstract/Ring.ML	Tue May 11 20:11:08 2004 +0200
     1.3 @@ -5,9 +5,9 @@
     1.4  *)
     1.5  
     1.6  (*
     1.7 -val a_assoc = thm "plus_ac0.assoc";
     1.8 -val l_zero = thm "plus_ac0.zero";
     1.9 -val a_comm = thm "plus_ac0.commute";
    1.10 +val a_assoc = thm "semigroup_add.add_assoc";
    1.11 +val l_zero = thm "comm_monoid_add.add_0";
    1.12 +val a_comm = thm "ab_semigroup_add.add_commute";
    1.13  
    1.14  section "Rings";
    1.15