src/HOL/Algebra/ROOT.ML
changeset 41413 64cd30d6b0b8
parent 35849 b5522b51cb1e
     1.1 --- a/src/HOL/Algebra/ROOT.ML	Wed Dec 29 13:51:17 2010 +0100
     1.2 +++ b/src/HOL/Algebra/ROOT.ML	Wed Dec 29 17:34:41 2010 +0100
     1.3 @@ -4,7 +4,12 @@
     1.4  *)
     1.5  
     1.6  (* Preliminaries from set and number theory *)
     1.7 -no_document use_thys ["FuncSet", "~~/src/HOL/Old_Number_Theory/Primes", "Binomial", "Permutation"];
     1.8 +no_document use_thys [
     1.9 +  "~~/src/HOL/Library/FuncSet",
    1.10 +  "~~/src/HOL/Old_Number_Theory/Primes",
    1.11 +  "~~/src/HOL/Library/Binomial",
    1.12 +  "~~/src/HOL/Library/Permutation"
    1.13 +];
    1.14  
    1.15  
    1.16  (*** New development, based on explicit structures ***)