don't distinguish between "fixes" and other free variables -- this confuses users
no_document use_thys [
"~~/src/HOL/Library/Infinite_Set",
"~~/src/HOL/Library/Permutation"
];
use_thys [
"Fib",
"Factorization",
"Chinese",
"WilsonRuss",
"WilsonBij",
"Quadratic_Reciprocity",
"Primes",
"Pocklington"
];