| changeset 19841 | f2fa72c13186 |
| parent 19770 | be5c23ebe1eb |
| child 19922 | 984ae977f7aa |
| 19840:600c35fd1b5e | 19841:f2fa72c13186 |
|---|---|
52 |
52 |
53 fun implies_elim_swp a b = implies_elim b a |
53 fun implies_elim_swp a b = implies_elim b a |
54 |
54 |
55 fun map3 _ [] [] [] = [] |
55 fun map3 _ [] [] [] = [] |
56 | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs |
56 | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs |
57 | map3 _ _ _ _ = raise UnequalLengths; |
57 | map3 _ _ _ _ = raise Library.UnequalLengths; |
58 |
58 |
59 |
59 |
60 |
60 |
61 (* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *) |
61 (* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *) |
62 fun upairs [] = [] |
62 fun upairs [] = [] |