src/HOL/Probability/Probability_Mass_Function.thy
changeset 63092 a949b2a5f51d
parent 63040 eb4ddd18d635
child 63099 af0e964aad7b
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Fri May 13 20:22:02 2016 +0200
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri May 13 20:24:10 2016 +0200
     1.3 @@ -653,7 +653,7 @@
     1.4  qed
     1.5  
     1.6  lemma set_embed_pmf: "set_pmf embed_pmf = {x. f x \<noteq> 0}"
     1.7 -by(auto simp add: set_pmf_eq assms pmf_embed_pmf)
     1.8 +by(auto simp add: set_pmf_eq pmf_embed_pmf)
     1.9  
    1.10  end
    1.11  
    1.12 @@ -1563,7 +1563,7 @@
    1.13                  ennreal_of_nat_eq_real_of_nat nn_integral_pmf_of_set)
    1.14  
    1.15  lemma measure_pmf_of_set: "measure (measure_pmf pmf_of_set) A = card (S \<inter> A) / card S"
    1.16 -  using emeasure_pmf_of_set[OF assms, of A]
    1.17 +  using emeasure_pmf_of_set[of A]
    1.18    by (simp add: measure_nonneg measure_pmf.emeasure_eq_measure)
    1.19  
    1.20  end