src/HOL/ROOT.ML
changeset 6392 e2ecfd8622ae
parent 6349 f7750d816c21
child 6431 a42bdc45130d
     1.1 --- a/src/HOL/ROOT.ML	Wed Mar 17 16:33:47 1999 +0100
     1.2 +++ b/src/HOL/ROOT.ML	Wed Mar 17 16:45:53 1999 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4  
     1.5  print_depth 1;
     1.6  
     1.7 -(* Add user sections *)
     1.8 +(*old-style theory syntax*)
     1.9  use "~~/src/Pure/section_utils.ML";
    1.10  use "thy_syntax.ML";
    1.11  
    1.12 @@ -56,8 +56,6 @@
    1.13  use "Tools/record_package.ML";
    1.14  use_thy "Record";
    1.15  
    1.16 -use_thy "Arith";
    1.17 -
    1.18  use_thy "Recdef";
    1.19  (*TFL: recursive function definitions*)
    1.20  cd "~~/src/TFL";