src/HOL/Library/Multiset.thy
changeset 55417 01fbfb60c33e
parent 55129 26bd1cba3ab5
child 55467 a5c9002bc54d
     1.1 --- a/src/HOL/Library/Multiset.thy	Wed Feb 12 08:35:57 2014 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Wed Feb 12 08:37:06 2014 +0100
     1.3 @@ -955,6 +955,7 @@
     1.4  lemma distinct_count_atmost_1:
     1.5    "distinct x = (! a. count (multiset_of x) a = (if a \<in> set x then 1 else 0))"
     1.6  apply (induct x, simp, rule iffI, simp_all)
     1.7 +apply (rename_tac a b)
     1.8  apply (rule conjI)
     1.9  apply (simp_all add: set_of_multiset_of [THEN sym] del: set_of_multiset_of)
    1.10  apply (erule_tac x = a in allE, simp, clarify)