tuned;
authorwenzelm
Wed, 17 Mar 1999 16:45:53 +0100
changeset 6392 e2ecfd8622ae
parent 6391 0da748358eff
child 6393 b8dafa978382
tuned;
src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Wed Mar 17 16:33:47 1999 +0100
+++ b/src/HOL/ROOT.ML	Wed Mar 17 16:45:53 1999 +0100
@@ -12,7 +12,7 @@
 
 print_depth 1;
 
-(* Add user sections *)
+(*old-style theory syntax*)
 use "~~/src/Pure/section_utils.ML";
 use "thy_syntax.ML";
 
@@ -56,8 +56,6 @@
 use "Tools/record_package.ML";
 use_thy "Record";
 
-use_thy "Arith";
-
 use_thy "Recdef";
 (*TFL: recursive function definitions*)
 cd "~~/src/TFL";