changeset 25140 | 273772abbea2 |
parent 25134 | 3d4953e88449 |
child 25162 | ad4d5365d9d8 |
--- a/src/HOL/Library/Multiset.thy Sun Oct 21 19:32:19 2007 +0200 +++ b/src/HOL/Library/Multiset.thy Sun Oct 21 22:33:35 2007 +0200 @@ -759,7 +759,7 @@ apply (rule_tac x = "x # xa" in exI, auto) done -lemma set_count_greater_0: "set x = {a. 0 < count (multiset_of x) a}" +lemma set_count_greater_0: "set x = {a. count (multiset_of x) a \<noteq> 0}" by (induct x) auto lemma distinct_count_atmost_1: