| changeset 19564 | d3e2f532459a |
| parent 19363 | 667b5ea637dd |
| child 19582 | a669c98b9c24 |
| 19563:ddd36d9e6943 | 19564:d3e2f532459a |
|---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* Multisets *} |
6 header {* Multisets *} |
7 |
7 |
8 theory Multiset |
8 theory Multiset |
9 imports Accessible_Part |
9 imports Main |
10 begin |
10 begin |
11 |
11 |
12 subsection {* The type of multisets *} |
12 subsection {* The type of multisets *} |
13 |
13 |
14 typedef 'a multiset = "{f::'a => nat. finite {x . 0 < f x}}" |
14 typedef 'a multiset = "{f::'a => nat. finite {x . 0 < f x}}" |