removed ML module DSeq which was a part of the ancient code generator (cf. 58e33a125f32)
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" ];