| changeset 60770 | 240563fbf41d |
| parent 58871 | c399ae4b836f |
| child 66453 | cc19f7ca2ed6 |
| 60769:cf7f3465eaf1 | 60770:240563fbf41d |
|---|---|
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 section {*Setsum for Multisets*} |
5 section \<open>Setsum for Multisets\<close> |
6 |
6 |
7 theory MultisetSum |
7 theory MultisetSum |
8 imports "../Induct/Multiset" |
8 imports "../Induct/Multiset" |
9 begin |
9 begin |
10 |
10 |