src/HOL/arith_data.ML
changeset 23085 fd30d75a6614
parent 22997 d4f3b015b50b
child 23190 d45c4d6c5f15
     1.1 --- a/src/HOL/arith_data.ML	Wed May 23 19:23:22 2007 +0200
     1.2 +++ b/src/HOL/arith_data.ML	Thu May 24 07:27:44 2007 +0200
     1.3 @@ -928,7 +928,7 @@
     1.4      lessD = lessD @ [thm "Suc_leI"],
     1.5      neqE = [@{thm linorder_neqE_nat}, @{thm linorder_neqE_ordered_idom}],
     1.6      simpset = HOL_basic_ss
     1.7 -      addsimps [@{thm "add_zero_left"}, @{thm "add_zero_right"},
     1.8 +      addsimps [@{thm "monoid_add_class.zero_plus.add_0_left"}, @{thm "monoid_add_class.zero_plus.add_0_right"},
     1.9          @{thm "Zero_not_Suc"}, @{thm "Suc_not_Zero"}, @{thm "le_0_eq"}, @{thm "One_nat_def"},
    1.10          @{thm "order_less_irrefl"}, @{thm "zero_neq_one"}, @{thm "zero_less_one"},
    1.11          @{thm "zero_le_one"}, @{thm "zero_neq_one"} RS not_sym, @{thm "not_one_le_zero"},