src/Pure/ROOT.ML
changeset 11882 954f36537193
parent 11835 13d12b99b843
child 11919 68b2578d4592
     1.1 --- a/src/Pure/ROOT.ML	Mon Oct 22 17:58:37 2001 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Mon Oct 22 17:58:56 2001 +0200
     1.3 @@ -45,20 +45,12 @@
     1.4  use "pure_thy.ML";
     1.5  use "drule.ML";
     1.6  use "meta_simplifier.ML";
     1.7 -use "locale.ML";
     1.8  use "tctical.ML";
     1.9  use "search.ML";
    1.10  use "tactic.ML";
    1.11 -use "goals.ML";
    1.12 -use "object_logic.ML";
    1.13  
    1.14  (*proof term operations*)
    1.15 -cd "Proof";
    1.16 -use "reconstruct.ML";
    1.17 -use "proof_syntax.ML";
    1.18 -use "proof_rewrite_rules.ML";
    1.19 -use "proofchecker.ML";
    1.20 -cd "..";
    1.21 +cd "Proof"; use "ROOT.ML"; cd "..";
    1.22  
    1.23  (*theory system operations*)
    1.24  cd "Thy"; use "ROOT.ML"; cd "..";
    1.25 @@ -66,9 +58,8 @@
    1.26  (*the Isar subsystem*)
    1.27  cd "Isar"; use "ROOT.ML"; cd "..";
    1.28  
    1.29 +use "goals.ML";
    1.30  use "axclass.ML";
    1.31 -
    1.32 -(*code generator*)
    1.33  use "codegen.ML";
    1.34  
    1.35  (*external interfaces*)