src/Pure/Isar/ROOT.ML
changeset 15703 727ef1b8b3ee
parent 15452 e2a721567f67
child 15709 f04c3d668c65
     1.1 --- a/src/Pure/Isar/ROOT.ML	Wed Apr 13 09:48:41 2005 +0200
     1.2 +++ b/src/Pure/Isar/ROOT.ML	Wed Apr 13 18:34:22 2005 +0200
     1.3 @@ -13,11 +13,11 @@
     1.4  use "proof_data.ML";
     1.5  use "delta_data.ML"; (*for delta_{claset,simpset}, part of SPASS interface*)
     1.6  use "context_rules.ML";
     1.7 +use "args.ML";
     1.8 +use "attrib.ML";
     1.9  use "locale.ML";
    1.10  use "proof.ML";
    1.11  use "proof_history.ML";
    1.12 -use "args.ML";
    1.13 -use "attrib.ML";
    1.14  use "net_rules.ML";
    1.15  use "induct_attrib.ML";
    1.16  use "method.ML";
    1.17 @@ -54,13 +54,16 @@
    1.18  struct
    1.19    structure ObjectLogic = ObjectLogic;
    1.20    structure AutoBind = AutoBind;
    1.21 +  structure RuleCases = RuleCases;
    1.22    structure ProofContext = ProofContext;
    1.23 +  structure ContextRules = ContextRules;
    1.24 +  structure Args = Args;
    1.25 +  structure Attrib = Attrib;
    1.26    structure Locale = Locale;
    1.27    structure Proof = Proof;
    1.28    structure ProofHistory = ProofHistory;
    1.29 -  structure Args = Args;
    1.30 -  structure Attrib = Attrib;
    1.31 -  structure ContextRules = ContextRules;
    1.32 +  structure NetRules = NetRules;
    1.33 +  structure InductAttrib = InductAttrib;
    1.34    structure Method = Method;
    1.35    structure Calculation = Calculation;
    1.36    structure Obtain = Obtain;