equal
deleted
inserted
replaced
2 |
2 |
3 section \<open>Discrete subprobability distribution\<close> |
3 section \<open>Discrete subprobability distribution\<close> |
4 |
4 |
5 theory SPMF imports |
5 theory SPMF imports |
6 Probability_Mass_Function |
6 Probability_Mass_Function |
7 Embed_Measure |
|
8 "~~/src/HOL/Library/Complete_Partial_Order2" |
7 "~~/src/HOL/Library/Complete_Partial_Order2" |
9 "~~/src/HOL/Library/Rewrite" |
8 "~~/src/HOL/Library/Rewrite" |
10 begin |
9 begin |
11 |
10 |
12 subsection \<open>Auxiliary material\<close> |
11 subsection \<open>Auxiliary material\<close> |