src/HOL/ROOT.ML
changeset 17919 09adb77ac16c
parent 16562 b74143e10410
child 18420 9470061ab283
     1.1 --- a/src/HOL/ROOT.ML	Wed Oct 19 21:52:30 2005 +0200
     1.2 +++ b/src/HOL/ROOT.ML	Wed Oct 19 21:52:31 2005 +0200
     1.3 @@ -9,9 +9,6 @@
     1.4  val banner = "Higher-Order Logic";
     1.5  writeln banner;
     1.6  
     1.7 -(*old-style theory syntax*)
     1.8 -use "thy_syntax.ML";
     1.9 -
    1.10  use "hologic.ML";
    1.11  
    1.12  use "~~/src/Provers/splitter.ML";