equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 section \<open>Code generation for PMFs\<close> |
8 section \<open>Code generation for PMFs\<close> |
9 |
9 |
10 theory PMF_Impl |
10 theory PMF_Impl |
11 imports Probability_Mass_Function "~~/src/HOL/Library/AList_Mapping" |
11 imports Probability_Mass_Function "HOL-Library.AList_Mapping" |
12 begin |
12 begin |
13 |
13 |
14 subsection \<open>General code generation setup\<close> |
14 subsection \<open>General code generation setup\<close> |
15 |
15 |
16 definition pmf_of_mapping :: "('a, real) mapping \<Rightarrow> 'a pmf" where |
16 definition pmf_of_mapping :: "('a, real) mapping \<Rightarrow> 'a pmf" where |