changeset 38052 | 04a8de29e8f7 |
parent 35408 | b48ab741683b |
child 42361 | 23f352990944 |
--- a/src/Provers/Arith/cancel_sums.ML Wed Jul 28 11:42:48 2010 +0200 +++ b/src/Provers/Arith/cancel_sums.ML Wed Jul 28 14:09:56 2010 +0200 @@ -35,7 +35,6 @@ fun cons1 x (xs, y, z) = (x :: xs, y, z); fun cons2 y (x, ys, z) = (x, y :: ys, z); -fun cons12 x y (xs, ys, z) = (x :: xs, y :: ys, z); (*symmetric difference of multisets -- assumed to be sorted wrt. Term_Ord.term_ord*) fun cancel ts [] vs = (ts, [], vs)