equal
deleted
inserted
replaced
882 end |
882 end |
883 |
883 |
884 fun isolate_monomials vars tm = |
884 fun isolate_monomials vars tm = |
885 let |
885 let |
886 val (cmons,vmons) = |
886 val (cmons,vmons) = |
887 List.partition (fn m => null (inter op aconvc (frees m, vars))) |
887 List.partition (fn m => null (inter (op aconvc) vars (frees m))) |
888 (striplist ring_dest_add tm) |
888 (striplist ring_dest_add tm) |
889 val cofactors = map (fn v => find_multipliers v vmons) vars |
889 val cofactors = map (fn v => find_multipliers v vmons) vars |
890 val cnc = if null cmons then zero_tm |
890 val cnc = if null cmons then zero_tm |
891 else Thm.capply ring_neg_tm |
891 else Thm.capply ring_neg_tm |
892 (list_mk_binop ring_add_tm cmons) |
892 (list_mk_binop ring_add_tm cmons) |