equal
deleted
inserted
replaced
11 typedecl |
11 typedecl |
12 'a multiset |
12 'a multiset |
13 |
13 |
14 consts |
14 consts |
15 |
15 |
16 "{|}" :: "'a multiset" ("{|}") |
16 emptym :: "'a multiset" ("{|}") |
17 addm :: "['a multiset, 'a] => 'a multiset" |
17 addm :: "['a multiset, 'a] => 'a multiset" |
18 delm :: "['a multiset, 'a] => 'a multiset" |
18 delm :: "['a multiset, 'a] => 'a multiset" |
19 countm :: "['a multiset, 'a => bool] => nat" |
19 countm :: "['a multiset, 'a => bool] => nat" |
20 count :: "['a multiset, 'a] => nat" |
20 count :: "['a multiset, 'a] => nat" |
21 |
21 |