equal
deleted
inserted
replaced
252 DiffCancelNumerals.proc)]; |
252 DiffCancelNumerals.proc)]; |
253 |
253 |
254 |
254 |
255 structure CombineNumeralsData = |
255 structure CombineNumeralsData = |
256 struct |
256 struct |
|
257 val add = op + : int*int -> int |
257 val mk_sum = long_mk_sum (*to work for e.g. #2*x + #3*x *) |
258 val mk_sum = long_mk_sum (*to work for e.g. #2*x + #3*x *) |
258 val dest_sum = dest_Sucs_sum |
259 val dest_sum = dest_Sucs_sum |
259 val mk_coeff = mk_coeff |
260 val mk_coeff = mk_coeff |
260 val dest_coeff = dest_coeff |
261 val dest_coeff = dest_coeff |
261 val left_distrib = left_add_mult_distrib RS trans |
262 val left_distrib = left_add_mult_distrib RS trans |