added helper -- cf. SET616^5
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" ];