no_document use_thys [ "~~/src/HOL/Library/Infinite_Set", "~~/src/HOL/Library/Permutation" ]; use_thys [ "Fib", "Factorization", "Chinese", "WilsonRuss", "WilsonBij", "Quadratic_Reciprocity", "Primes", "Pocklington" ];