maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
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" ];