equal
deleted
inserted
replaced
525 definition "equal_pmf p q = (mapping_of_pmf p = mapping_of_pmf (q :: 'a pmf))" |
525 definition "equal_pmf p q = (mapping_of_pmf p = mapping_of_pmf (q :: 'a pmf))" |
526 |
526 |
527 instance by standard (simp add: equal_pmf_def) |
527 instance by standard (simp add: equal_pmf_def) |
528 end |
528 end |
529 |
529 |
|
530 definition single :: "'a \<Rightarrow> 'a multiset" where |
|
531 "single s = {#s#}" |
530 |
532 |
531 definition (in term_syntax) |
533 definition (in term_syntax) |
532 pmfify :: "('a::typerep multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<Rightarrow> |
534 pmfify :: "('a::typerep multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<Rightarrow> |
533 'a \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> |
535 'a \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> |
534 'a pmf \<times> (unit \<Rightarrow> Code_Evaluation.term)" where |
536 'a pmf \<times> (unit \<Rightarrow> Code_Evaluation.term)" where |