src/HOL/Probability/Probability_Mass_Function.thy
changeset 60495 d7ff0a1df90a
parent 60068 ef2123db900c
child 60595 804dfdc82835
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Jun 16 20:50:00 2015 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Wed Jun 17 17:21:11 2015 +0200
     1.3 @@ -1413,7 +1413,7 @@
     1.4  lemma pmf_of_multiset[simp]: "pmf pmf_of_multiset x = count M x / size M"
     1.5    by transfer rule
     1.6  
     1.7 -lemma set_pmf_of_multiset[simp]: "set_pmf pmf_of_multiset = set_of M"
     1.8 +lemma set_pmf_of_multiset[simp]: "set_pmf pmf_of_multiset = set_mset M"
     1.9    by (auto simp: set_pmf_iff)
    1.10  
    1.11  end