equal
deleted
inserted
replaced
43 qed "int_nat_number_of"; |
43 qed "int_nat_number_of"; |
44 Addsimps [int_nat_number_of]; |
44 Addsimps [int_nat_number_of]; |
45 |
45 |
46 |
46 |
47 val nat_bin_arith_setup = |
47 val nat_bin_arith_setup = |
48 [Fast_Arith.map_data (fn {add_mono_thms, inj_thms, lessD, simpset} => |
48 [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => |
49 {add_mono_thms = add_mono_thms, |
49 {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, |
50 inj_thms = inj_thms, |
50 inj_thms = inj_thms, |
51 lessD = lessD, |
51 lessD = lessD, |
52 simpset = simpset addsimps [int_nat_number_of, |
52 simpset = simpset addsimps [int_nat_number_of, |
53 not_neg_number_of_Pls,neg_number_of_Min,neg_number_of_BIT]})]; |
53 not_neg_number_of_Pls,neg_number_of_Min,neg_number_of_BIT]})]; |
54 |
54 |