src/Pure/Isar/ROOT.ML
changeset 15703 727ef1b8b3ee
parent 15452 e2a721567f67
child 15709 f04c3d668c65
--- a/src/Pure/Isar/ROOT.ML	Wed Apr 13 09:48:41 2005 +0200
+++ b/src/Pure/Isar/ROOT.ML	Wed Apr 13 18:34:22 2005 +0200
@@ -13,11 +13,11 @@
 use "proof_data.ML";
 use "delta_data.ML"; (*for delta_{claset,simpset}, part of SPASS interface*)
 use "context_rules.ML";
+use "args.ML";
+use "attrib.ML";
 use "locale.ML";
 use "proof.ML";
 use "proof_history.ML";
-use "args.ML";
-use "attrib.ML";
 use "net_rules.ML";
 use "induct_attrib.ML";
 use "method.ML";
@@ -54,13 +54,16 @@
 struct
   structure ObjectLogic = ObjectLogic;
   structure AutoBind = AutoBind;
+  structure RuleCases = RuleCases;
   structure ProofContext = ProofContext;
+  structure ContextRules = ContextRules;
+  structure Args = Args;
+  structure Attrib = Attrib;
   structure Locale = Locale;
   structure Proof = Proof;
   structure ProofHistory = ProofHistory;
-  structure Args = Args;
-  structure Attrib = Attrib;
-  structure ContextRules = ContextRules;
+  structure NetRules = NetRules;
+  structure InductAttrib = InductAttrib;
   structure Method = Method;
   structure Calculation = Calculation;
   structure Obtain = Obtain;