changeset 73297 | beaff25452d2 |
parent 70347 | e5cd5471c18a |
child 73392 | 24f0df084aad |
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Tue Feb 23 20:41:48 2021 +0000 +++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Tue Feb 23 20:41:48 2021 +0000 @@ -3,7 +3,7 @@ section \<open>Formalization of a Countermeasure by Koepf \& Duermuth 2009\<close> theory Koepf_Duermuth_Countermeasure - imports "HOL-Probability.Information" "HOL-Library.Permutation" + imports "HOL-Probability.Information" "HOL-Library.List_Permutation" begin lemma SIGMA_image_vimage: