src/HOL/NumberTheory/ROOT.ML
changeset 11049 7eef34adb852
parent 9944 2a705d1af4dc
child 11368 9c1995c73383
     1.1 --- a/src/HOL/NumberTheory/ROOT.ML	Sat Feb 03 17:43:34 2001 +0100
     1.2 +++ b/src/HOL/NumberTheory/ROOT.ML	Sun Feb 04 19:31:13 2001 +0100
     1.3 @@ -1,15 +1,10 @@
     1.4 -(*  Title:      HOL/NumberTheory/ROOT
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   2000  University of Cambridge
     1.8  
     1.9 -Number theory developments by Thomas M Rasmussen
    1.10 -*)
    1.11 +no_document use_thy "Permutation";
    1.12  
    1.13 -time_use_thy "Primes";
    1.14 -time_use_thy "Fib";
    1.15 -with_path "../Induct" time_use_thy "Factorization";
    1.16 -time_use_thy "Chinese";
    1.17 -time_use_thy "EulerFermat";
    1.18 -time_use_thy "WilsonRuss";
    1.19 -time_use_thy "WilsonBij";
    1.20 +use_thy "Primes";
    1.21 +use_thy "Fib";
    1.22 +use_thy "Factorization";
    1.23 +use_thy "Chinese";
    1.24 +use_thy "EulerFermat";
    1.25 +use_thy "WilsonRuss";
    1.26 +use_thy "WilsonBij";