eliminated unnecessary tail-recursion and funny use of records as 'named arguments' for functions
no_document use_thys [
"~~/src/HOL/Library/Infinite_Set",
"~~/src/HOL/Library/Permutation"
];
use_thys [
"Fib",
"Factorization",
"Chinese",
"WilsonRuss",
"WilsonBij",
"Quadratic_Reciprocity",
"Primes",
"Pocklington"
];