equal
deleted
inserted
replaced
625 LinArith.map_data |
625 LinArith.map_data |
626 (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => |
626 (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => |
627 {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, |
627 {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, |
628 inj_thms = inj_thms, |
628 inj_thms = inj_thms, |
629 lessD = lessD, neqE = neqE, |
629 lessD = lessD, neqE = neqE, |
630 simpset = simpset addsimps [Suc_nat_number_of, int_nat_number_of, |
630 simpset = simpset addsimps @{thms neg_simps} @ |
631 @{thm not_neg_number_of_Pls}, @{thm neg_number_of_Min}, |
631 [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}]}) |
632 @{thm neg_number_of_Bit0}, @{thm neg_number_of_Bit1}]}) |
|
633 *} |
632 *} |
634 |
633 |
635 declaration {* K nat_bin_arith_setup *} |
634 declaration {* K nat_bin_arith_setup *} |
636 |
635 |
637 (* Enable arith to deal with div/mod k where k is a numeral: *) |
636 (* Enable arith to deal with div/mod k where k is a numeral: *) |