| changeset 9659 | b9cf6801f3da |
| parent 9017 | ff259b415c4d |
| 9658:97d6d0a72d35 | 9659:b9cf6801f3da |
|---|---|
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1998 TUM |
4 Copyright 1998 TUM |
5 |
5 |
6 A definitional theory of multisets, |
6 A definitional theory of multisets, |
7 including a wellfoundedness proof for the multiset order. |
7 including a wellfoundedness proof for the multiset order. |
8 use_thy"Multiset"; |
|
9 |
|
10 *) |
8 *) |
11 |
9 |
12 Multiset = Multiset0 + Acc + |
10 Multiset = Multiset0 + Acc + |
13 |
11 |
14 typedef |
12 typedef |