changeset 5017 | 786a17461ab9 |
parent 5004 | cf4e3b487caf |
child 5092 | e443bc494604 |
--- a/src/Pure/ROOT.ML Wed Jun 10 11:54:04 1998 +0200 +++ b/src/Pure/ROOT.ML Wed Jun 10 11:55:09 1998 +0200 @@ -13,12 +13,9 @@ ml_prompts "> " "# "; -(*basic utils*) +(*basic tools*) use "library.ML"; -use "table.ML"; -use "object.ML"; -use "seq.ML"; -use "name_space.ML"; +cd "General"; use "ROOT.ML"; cd ".."; use "term.ML"; (*inner syntax module*)