equal
deleted
inserted
replaced
106 bin_minus_type, bin_add_type, bin_mult_type]; |
106 bin_minus_type, bin_add_type, bin_mult_type]; |
107 |
107 |
108 val bin_ss = integ_ss |
108 val bin_ss = integ_ss |
109 addsimps([bool_1I, bool_0I, |
109 addsimps([bool_1I, bool_0I, |
110 bin_rec_Plus, bin_rec_Minus, bin_rec_Bcons] @ |
110 bin_rec_Plus, bin_rec_Minus, bin_rec_Bcons] @ |
111 bin_recs integ_of_bin_def @ bool_rews @ bin_typechecks); |
111 bin_recs integ_of_bin_def @ bool_simps @ bin_typechecks); |
112 |
112 |
113 val typechecks = bin_typechecks @ integ_typechecks @ nat_typechecks @ |
113 val typechecks = bin_typechecks @ integ_typechecks @ nat_typechecks @ |
114 [bool_subset_nat RS subsetD]; |
114 [bool_subset_nat RS subsetD]; |
115 |
115 |
116 (**** The carry/borrow functions, bin_succ and bin_pred ****) |
116 (**** The carry/borrow functions, bin_succ and bin_pred ****) |