# HG changeset patch
# User wenzelm
# Date 911905190 -3600
# Node ID e98c900540f9325daf8aa148c512c2c7bcd218e5
# Parent  d218409fd44e126be54484c63ffd462b1e1d4cbd
added isar.ML;

diff -r d218409fd44e -r e98c900540f9 src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Tue Nov 24 11:59:35 1998 +0100
+++ b/src/Pure/Isar/ROOT.ML	Tue Nov 24 11:59:50 1998 +0100
@@ -27,6 +27,8 @@
 use "isar_cmd.ML";
 use "isar_syn.ML";
 
+(*main interface*)
+use "isar.ML";
 
 structure PureIsar =
 struct
@@ -43,4 +45,5 @@
   structure IsarThy = IsarThy;
   structure IsarCmd = IsarCmd;
   structure IsarSyn = IsarSyn;
+  structure Isar = Isar;
 end;