src/Pure/Isar/ROOT.ML
changeset 5873 f4fe91b3b6db
parent 5818 962bfe78a297
child 5951 e98c900540f9
--- a/src/Pure/Isar/ROOT.ML	Mon Nov 16 10:44:30 1998 +0100
+++ b/src/Pure/Isar/ROOT.ML	Mon Nov 16 10:44:55 1998 +0100
@@ -26,3 +26,21 @@
 use "isar_thy.ML";
 use "isar_cmd.ML";
 use "isar_syn.ML";
+
+
+structure PureIsar =
+struct
+  structure ProofContext = ProofContext;
+  structure Proof = Proof;
+  structure Args = Args;
+  structure Attrib = Attrib;
+  structure Method = Method;
+  structure OuterLex = OuterLex;
+  structure OuterParse = OuterParse;
+  structure ProofHistory = ProofHistory;
+  structure Toplevel = Toplevel;
+  structure OuterSyntax = OuterSyntax;
+  structure IsarThy = IsarThy;
+  structure IsarCmd = IsarCmd;
+  structure IsarSyn = IsarSyn;
+end;