add theory data for relator identity rules;
preprocess transfer rules generated by lift_definition using relator rules
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" ];