equal
deleted
inserted
replaced
654 {* |
654 {* |
655 val numerals = thms"numerals"; |
655 val numerals = thms"numerals"; |
656 val numeral_ss = simpset() addsimps numerals; |
656 val numeral_ss = simpset() addsimps numerals; |
657 |
657 |
658 val nat_bin_arith_setup = |
658 val nat_bin_arith_setup = |
659 Fast_Arith.map_data |
659 LinArith.map_data |
660 (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => |
660 (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => |
661 {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, |
661 {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, |
662 inj_thms = inj_thms, |
662 inj_thms = inj_thms, |
663 lessD = lessD, neqE = neqE, |
663 lessD = lessD, neqE = neqE, |
664 simpset = simpset addsimps [Suc_nat_number_of, int_nat_number_of, |
664 simpset = simpset addsimps [Suc_nat_number_of, int_nat_number_of, |