# HG changeset patch # User wenzelm # Date 897472509 -7200 # Node ID 786a17461ab9f920f3c8e01590bb030202327051 # Parent 67c5966611c680e39bbd895d4e96f8b96a06d77a moved table.ML, object.ML, seq.ML, name_space.ML to General; diff -r 67c5966611c6 -r 786a17461ab9 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Wed Jun 10 11:54:04 1998 +0200 +++ b/src/Pure/IsaMakefile Wed Jun 10 11:55:09 1998 +0200 @@ -23,20 +23,20 @@ Pure: $(OUT)/Pure -$(OUT)/Pure: ML-Systems/mlworks.ML ML-Systems/polyml.ML \ - ML-Systems/smlnj-0.93.ML ML-Systems/smlnj.ML ROOT.ML Syntax/ROOT.ML \ - Syntax/ast.ML Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \ - Syntax/pretty.ML Syntax/printer.ML Syntax/scan.ML Syntax/source.ML \ - Syntax/symbol.ML Syntax/syn_ext.ML Syntax/syn_trans.ML \ - Syntax/syntax.ML Syntax/token_trans.ML Syntax/type_ext.ML \ - Thy/ROOT.ML Thy/browser_info.ML Thy/context.ML Thy/file.ML \ - Thy/path.ML Thy/position.ML Thy/thm_database.ML Thy/thy_info.ML \ +$(OUT)/Pure: General/file.ML General/name_space.ML General/object.ML \ + General/path.ML General/position.ML General/seq.ML General/table.ML \ + ML-Systems/mlworks.ML ML-Systems/polyml.ML ML-Systems/smlnj-0.93.ML \ + ML-Systems/smlnj.ML ROOT.ML Syntax/ROOT.ML Syntax/ast.ML \ + Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML Syntax/pretty.ML \ + Syntax/printer.ML Syntax/scan.ML Syntax/source.ML Syntax/symbol.ML \ + Syntax/syn_ext.ML Syntax/syn_trans.ML Syntax/syntax.ML \ + Syntax/token_trans.ML Syntax/type_ext.ML Thy/ROOT.ML \ + Thy/browser_info.ML Thy/context.ML Thy/thm_database.ML Thy/thy_info.ML \ Thy/thy_parse.ML Thy/thy_read.ML Thy/thy_scan.ML Thy/thy_syn.ML \ Thy/use.ML attribute.ML axclass.ML basis.ML deriv.ML display.ML \ - drule.ML envir.ML goals.ML install_pp.ML library.ML logic.ML \ - name_space.ML net.ML object.ML pattern.ML pure_thy.ML search.ML \ - seq.ML sign.ML sorts.ML table.ML tactic.ML tctical.ML term.ML \ - theory.ML theory_data.ML thm.ML type.ML type_infer.ML unify.ML + drule.ML envir.ML goals.ML install_pp.ML library.ML logic.ML net.ML \ + pattern.ML pure_thy.ML search.ML sign.ML sorts.ML tactic.ML tctical.ML \ + term.ML theory.ML theory_data.ML thm.ML type.ML type_infer.ML unify.ML @./mk diff -r 67c5966611c6 -r 786a17461ab9 src/Pure/ROOT.ML --- 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*)