src/HOL/ROOT.ML
changeset 8812 7239b21e2068
parent 8786 2f3412cd1b68
child 9157 998dd2fb5795
     1.1 --- a/src/HOL/ROOT.ML	Fri May 05 22:24:47 2000 +0200
     1.2 +++ b/src/HOL/ROOT.ML	Fri May 05 22:25:17 2000 +0200
     1.3 @@ -12,7 +12,6 @@
     1.4  print_depth 1;
     1.5  
     1.6  (*old-style theory syntax*)
     1.7 -use "~~/src/Pure/section_utils.ML";
     1.8  use "thy_syntax.ML";
     1.9  
    1.10  use "hologic.ML";