equal
deleted
inserted
replaced
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson |
3 Author: Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 *) |
5 *) |
6 |
6 |
7 header {* |
7 header {* Multisets *} |
8 \title{Multisets} |
|
9 \author{Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson} |
|
10 *} |
|
11 |
8 |
12 theory Multiset = Accessible_Part: |
9 theory Multiset = Accessible_Part: |
13 |
10 |
14 subsection {* The type of multisets *} |
11 subsection {* The type of multisets *} |
15 |
12 |