| changeset 15140 | 322485b816ac |
| parent 15131 | c69542757a4d |
| child 15316 | 2a6ff941a115 |
| 15139:58cd3404cf75 | 15140:322485b816ac |
|---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* Multisets *} |
6 header {* Multisets *} |
7 |
7 |
8 theory Multiset |
8 theory Multiset |
9 import Accessible_Part |
9 imports Accessible_Part |
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}}" |