equal
deleted
inserted
replaced
3 Author: Tobias Nipkow, Markus Wenzel, Lawrence C Paulson, Norbert Voelker |
3 Author: Tobias Nipkow, Markus Wenzel, Lawrence C Paulson, Norbert Voelker |
4 *) |
4 *) |
5 |
5 |
6 header {* Multisets *} |
6 header {* Multisets *} |
7 |
7 |
8 theory Multiset = Accessible_Part: |
8 theory Multiset |
|
9 import Accessible_Part |
|
10 begin |
9 |
11 |
10 subsection {* The type of multisets *} |
12 subsection {* The type of multisets *} |
11 |
13 |
12 typedef 'a multiset = "{f::'a => nat. finite {x . 0 < f x}}" |
14 typedef 'a multiset = "{f::'a => nat. finite {x . 0 < f x}}" |
13 proof |
15 proof |