changeset 7370 | 6407a09ac58f |
parent 7357 | d0e16da40ea2 |
child 7548 | 9e29a3af64ab |
--- a/src/HOL/ROOT.ML Thu Aug 26 19:04:19 1999 +0200 +++ b/src/HOL/ROOT.ML Thu Aug 26 19:04:26 1999 +0200 @@ -15,6 +15,7 @@ (*old-style theory syntax*) use "~~/src/Pure/section_utils.ML"; use "thy_syntax.ML"; + use "hologic.ML"; use "~~/src/Provers/simplifier.ML"; @@ -34,7 +35,6 @@ use_thy "subset"; use "Tools/typedef_package.ML"; - use_thy "Inductive"; use_thy "NatDef";