src/HOL/Old_Number_Theory/ROOT.ML
changeset 32479 521cc9bf2958
parent 24104 719fbe4fb77f
child 41413 64cd30d6b0b8
equal deleted inserted replaced
32478:87201c60ae7d 32479:521cc9bf2958
       
     1 
       
     2 no_document use_thys ["Infinite_Set", "Permutation"];
       
     3 use_thys ["Fib", "Factorization", "Chinese", "WilsonRuss",
       
     4   "WilsonBij", "Quadratic_Reciprocity", "Primes", "Pocklington"];