src/HOL/ROOT.ML
changeset 5105 0ff5bec04d02
parent 5097 6c4a7ad6ebc7
child 5107 2edf5dfb02f3
     1.1 --- a/src/HOL/ROOT.ML	Wed Jul 01 11:20:32 1998 +0200
     1.2 +++ b/src/HOL/ROOT.ML	Wed Jul 01 11:33:39 1998 +0200
     1.3 @@ -36,7 +36,8 @@
     1.4  use_thy "Ord";
     1.5  use_thy "subset";
     1.6  use "Tools/typedef_package.ML";
     1.7 -use_thy "Inductive";
     1.8 +use_thy "Sum";
     1.9 +use_thy "Gfp";
    1.10  
    1.11  use "Tools/record_package.ML";
    1.12  use_thy "Record";
    1.13 @@ -46,6 +47,7 @@
    1.14  use "arith_data.ML";
    1.15  
    1.16  use "Tools/inductive_package.ML";
    1.17 +use_thy "Inductive";
    1.18  
    1.19  use_thy "RelPow";
    1.20  use_thy "Finite";