801 inj_thms = inj_thms, |
801 inj_thms = inj_thms, |
802 lessD = lessD @ [thm "Suc_leI"], |
802 lessD = lessD @ [thm "Suc_leI"], |
803 neqE = [@{thm linorder_neqE_nat}, @{thm linorder_neqE_ordered_idom}], |
803 neqE = [@{thm linorder_neqE_nat}, @{thm linorder_neqE_ordered_idom}], |
804 simpset = HOL_basic_ss |
804 simpset = HOL_basic_ss |
805 addsimps |
805 addsimps |
806 [@{thm "monoid_add_class.zero_plus.add_0_left"}, |
806 [@{thm "monoid_add_class.add_0_left"}, |
807 @{thm "monoid_add_class.zero_plus.add_0_right"}, |
807 @{thm "monoid_add_class.add_0_right"}, |
808 @{thm "Zero_not_Suc"}, @{thm "Suc_not_Zero"}, @{thm "le_0_eq"}, @{thm "One_nat_def"}, |
808 @{thm "Zero_not_Suc"}, @{thm "Suc_not_Zero"}, @{thm "le_0_eq"}, @{thm "One_nat_def"}, |
809 @{thm "order_less_irrefl"}, @{thm "zero_neq_one"}, @{thm "zero_less_one"}, |
809 @{thm "order_less_irrefl"}, @{thm "zero_neq_one"}, @{thm "zero_less_one"}, |
810 @{thm "zero_le_one"}, @{thm "zero_neq_one"} RS not_sym, @{thm "not_one_le_zero"}, |
810 @{thm "zero_le_one"}, @{thm "zero_neq_one"} RS not_sym, @{thm "not_one_le_zero"}, |
811 @{thm "not_one_less_zero"}] |
811 @{thm "not_one_less_zero"}] |
812 addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv] |
812 addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv] |