author | wenzelm |
Wed, 17 Mar 1999 16:45:53 +0100 | |
changeset 6392 | e2ecfd8622ae |
parent 6391 | 0da748358eff |
child 6393 | b8dafa978382 |
src/HOL/ROOT.ML | file | annotate | diff | comparison | revisions |
--- 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";