| changeset 58871 | c399ae4b836f |
| parent 46823 | 57bf0cecb366 |
| child 60770 | 240563fbf41d |
| 58870:e2c0d8ef29cb | 58871:c399ae4b836f |
|---|---|
1 (* Title: ZF/UNITY/MultisetSum.thy |
1 (* Title: ZF/UNITY/MultisetSum.thy |
2 Author: Sidi O Ehmety |
2 Author: Sidi O Ehmety |
3 *) |
3 *) |
4 |
4 |
5 header {*Setsum for Multisets*} |
5 section {*Setsum for Multisets*} |
6 |
6 |
7 theory MultisetSum |
7 theory MultisetSum |
8 imports "../Induct/Multiset" |
8 imports "../Induct/Multiset" |
9 begin |
9 begin |
10 |
10 |