src/HOL/ROOT.ML
changeset 7370 6407a09ac58f
parent 7357 d0e16da40ea2
child 7548 9e29a3af64ab
     1.1 --- a/src/HOL/ROOT.ML	Thu Aug 26 19:04:19 1999 +0200
     1.2 +++ b/src/HOL/ROOT.ML	Thu Aug 26 19:04:26 1999 +0200
     1.3 @@ -15,6 +15,7 @@
     1.4  (*old-style theory syntax*)
     1.5  use "~~/src/Pure/section_utils.ML";
     1.6  use "thy_syntax.ML";
     1.7 +
     1.8  use "hologic.ML";
     1.9  
    1.10  use "~~/src/Provers/simplifier.ML";
    1.11 @@ -34,7 +35,6 @@
    1.12  
    1.13  use_thy "subset";
    1.14  use "Tools/typedef_package.ML";
    1.15 -
    1.16  use_thy "Inductive";
    1.17  use_thy "NatDef";
    1.18