| changeset 12338 | de0f4a63baa5 |
| parent 12218 | 6597093b77e7 |
| child 14981 | e73f8140af78 |
| 12337:7c6a970f0808 | 12338:de0f4a63baa5 |
|---|---|
13 |
13 |
14 'a multiset |
14 'a multiset |
15 |
15 |
16 arities |
16 arities |
17 |
17 |
18 multiset :: (term) term |
18 multiset :: (type) type |
19 |
19 |
20 consts |
20 consts |
21 |
21 |
22 "{|}" :: 'a multiset ("{|}") |
22 "{|}" :: 'a multiset ("{|}") |
23 addm :: ['a multiset, 'a] => 'a multiset |
23 addm :: ['a multiset, 'a] => 'a multiset |