816 @{thm add_0_right}, |
816 @{thm add_0_right}, |
817 @{thm "Zero_not_Suc"}, @{thm "Suc_not_Zero"}, @{thm "le_0_eq"}, @{thm "One_nat_def"}, |
817 @{thm "Zero_not_Suc"}, @{thm "Suc_not_Zero"}, @{thm "le_0_eq"}, @{thm "One_nat_def"}, |
818 @{thm "order_less_irrefl"}, @{thm "zero_neq_one"}, @{thm "zero_less_one"}, |
818 @{thm "order_less_irrefl"}, @{thm "zero_neq_one"}, @{thm "zero_less_one"}, |
819 @{thm "zero_le_one"}, @{thm "zero_neq_one"} RS not_sym, @{thm "not_one_le_zero"}, |
819 @{thm "zero_le_one"}, @{thm "zero_neq_one"} RS not_sym, @{thm "not_one_le_zero"}, |
820 @{thm "not_one_less_zero"}] |
820 @{thm "not_one_less_zero"}] |
821 addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv] |
821 addsimprocs [Abel_Cancel.sum_conv, Abel_Cancel.rel_conv] |
822 (*abel_cancel helps it work in abstract algebraic domains*) |
822 (*abel_cancel helps it work in abstract algebraic domains*) |
823 addsimprocs Nat_Arith.nat_cancel_sums_add |
823 addsimprocs Nat_Arith.nat_cancel_sums_add |
824 addcongs [@{thm if_weak_cong}], |
824 addcongs [@{thm if_weak_cong}], |
825 number_of = number_of}) #> |
825 number_of = number_of}) #> |
826 add_discrete_type @{type_name nat}; |
826 add_discrete_type @{type_name nat}; |