src/HOL/Probability/Probability_Mass_Function.thy
changeset 63343 fb5d8a50c641
parent 63194 0b7bdb75f451
child 63540 f8652d0534fa
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Jun 21 17:35:45 2016 +0200
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Wed Jun 22 10:09:20 2016 +0200
     1.3 @@ -1775,7 +1775,8 @@
     1.4  lemma set_pmf_binomial[simp]: "0 < p \<Longrightarrow> p < 1 \<Longrightarrow> set_pmf (binomial_pmf n p) = {..n}"
     1.5    by (simp add: set_pmf_binomial_eq)
     1.6  
     1.7 -context begin interpretation lifting_syntax .
     1.8 +context includes lifting_syntax
     1.9 +begin
    1.10  
    1.11  lemma bind_pmf_parametric [transfer_rule]:
    1.12    "(rel_pmf A ===> (A ===> rel_pmf B) ===> rel_pmf B) bind_pmf bind_pmf"