no_document use_thys [ "~~/src/HOL/Library/Countable", "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits", "~~/src/HOL/Library/Permutation"]; use_thys [ "Probability", "ex/Dining_Cryptographers", "ex/Koepf_Duermuth_Countermeasure" ];