src/HOL/Divides.thy
changeset 35050 9f841f20dca6
parent 34982 7b8c366e34a2
child 35216 7641e8d831d2
     1.1 --- a/src/HOL/Divides.thy	Mon Feb 08 17:12:32 2010 +0100
     1.2 +++ b/src/HOL/Divides.thy	Mon Feb 08 17:12:38 2010 +0100
     1.3 @@ -657,7 +657,7 @@
     1.4    val trans = trans;
     1.5  
     1.6    val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
     1.7 -    (@{thm monoid_add_class.add_0_left} :: @{thm monoid_add_class.add_0_right} :: @{thms add_ac}))
     1.8 +    (@{thm add_0_left} :: @{thm add_0_right} :: @{thms add_ac}))
     1.9  
    1.10  end)
    1.11  
    1.12 @@ -1655,8 +1655,8 @@
    1.13  lemmas arithmetic_simps =
    1.14    arith_simps
    1.15    add_special
    1.16 -  OrderedGroup.add_0_left
    1.17 -  OrderedGroup.add_0_right
    1.18 +  add_0_left
    1.19 +  add_0_right
    1.20    mult_zero_left
    1.21    mult_zero_right
    1.22    mult_1_left