--- a/src/Pure/IsaMakefile Fri May 21 16:22:39 1999 +0200
+++ b/src/Pure/IsaMakefile Fri May 21 16:23:18 1999 +0200
@@ -27,7 +27,8 @@
General/graph.ML General/history.ML General/name_space.ML \
General/object.ML General/path.ML General/position.ML \
General/pretty.ML General/scan.ML General/seq.ML General/source.ML \
- General/symbol.ML General/table.ML General/url.ML Isar/ROOT.ML \
+ General/symbol.ML General/table.ML General/url.ML Interface/ROOT.ML \
+ Interface/isamode.ML Interface/proof_general.ML Isar/ROOT.ML \
Isar/args.ML Isar/attrib.ML Isar/comment.ML Isar/isar.ML \
Isar/isar_cmd.ML Isar/isar_syn.ML Isar/isar_thy.ML Isar/method.ML \
Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML \
--- a/src/Pure/ROOT.ML Fri May 21 16:22:39 1999 +0200
+++ b/src/Pure/ROOT.ML Fri May 21 16:23:18 1999 +0200
@@ -57,8 +57,12 @@
(*the Isar subsystem*)
cd "Isar"; use "ROOT.ML"; cd "..";
+use "axclass.ML";
+
+(*external interfaces*)
+cd "Interface"; use "ROOT.ML"; cd "..";
+
(*final Pure theory setup*)
-use "axclass.ML";
use "pure.ML";
(*several object-logics declare theories that hide basis library structures*)