src/Pure/ROOT.ML
changeset 56206 7adec2a527f5
parent 56205 ceb8a93460b7
child 56208 06cc31dff138
     1.1 --- a/src/Pure/ROOT.ML	Tue Mar 18 16:16:28 2014 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Tue Mar 18 16:44:51 2014 +0100
     1.3 @@ -211,12 +211,6 @@
     1.4  use "Syntax/syntax_phases.ML";
     1.5  use "Isar/local_defs.ML";
     1.6  
     1.7 -(*proof term operations*)
     1.8 -use "Proof/reconstruct.ML";
     1.9 -use "Proof/proof_syntax.ML";
    1.10 -use "Proof/proof_rewrite_rules.ML";
    1.11 -use "Proof/proof_checker.ML";
    1.12 -
    1.13  (*outer syntax*)
    1.14  use "Isar/token.ML";
    1.15  use "Isar/keyword.ML";
    1.16 @@ -271,6 +265,13 @@
    1.17  use "Isar/proof_node.ML";
    1.18  use "Isar/toplevel.ML";
    1.19  
    1.20 +(*proof term operations*)
    1.21 +use "Proof/reconstruct.ML";
    1.22 +use "Proof/proof_syntax.ML";
    1.23 +use "Proof/proof_rewrite_rules.ML";
    1.24 +use "Proof/proof_checker.ML";
    1.25 +use "Proof/extraction.ML";
    1.26 +
    1.27  (*theory documents*)
    1.28  use "System/isabelle_system.ML";
    1.29  use "Thy/term_style.ML";
    1.30 @@ -290,8 +291,6 @@
    1.31  
    1.32  use "subgoal.ML";
    1.33  
    1.34 -use "Proof/extraction.ML";
    1.35 -
    1.36  
    1.37  (* Isabelle/Isar system *)
    1.38