src/HOL/Old_Number_Theory/ROOT.ML
changeset 41413 64cd30d6b0b8
parent 32479 521cc9bf2958
     1.1 --- a/src/HOL/Old_Number_Theory/ROOT.ML	Wed Dec 29 13:51:17 2010 +0100
     1.2 +++ b/src/HOL/Old_Number_Theory/ROOT.ML	Wed Dec 29 17:34:41 2010 +0100
     1.3 @@ -1,4 +1,15 @@
     1.4 +no_document use_thys [
     1.5 +  "~~/src/HOL/Library/Infinite_Set",
     1.6 +  "~~/src/HOL/Library/Permutation"
     1.7 +];
     1.8  
     1.9 -no_document use_thys ["Infinite_Set", "Permutation"];
    1.10 -use_thys ["Fib", "Factorization", "Chinese", "WilsonRuss",
    1.11 -  "WilsonBij", "Quadratic_Reciprocity", "Primes", "Pocklington"];
    1.12 +use_thys [
    1.13 +  "Fib",
    1.14 +  "Factorization",
    1.15 +  "Chinese",
    1.16 +  "WilsonRuss",
    1.17 +  "WilsonBij",
    1.18 +  "Quadratic_Reciprocity",
    1.19 +  "Primes",
    1.20 +  "Pocklington"
    1.21 +];