changeset 45713 | badee348c5fb |
parent 33615 | 261abc2e3155 |
45712:852597248663 | 45713:badee348c5fb |
---|---|
1 use_thys ["Probability"]; |
1 no_document use_thys [ |
2 "~~/src/HOL/Library/Countable", |
|
3 "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits", |
|
4 "~~/src/HOL/Library/Permutation"]; |
|
5 |
|
6 use_thys [ |
|
7 "Probability", |
|
8 "ex/Dining_Cryptographers", |
|
9 "ex/Koepf_Duermuth_Countermeasure" ]; |