tuned;
authorwenzelm
Thu Aug 26 19:04:26 1999 +0200 (1999-08-26)
changeset 73706407a09ac58f
parent 7369 2d2110cda81e
child 7371 b176626f0d80
tuned;
src/HOL/ROOT.ML
     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