# HG changeset patch
# User wenzelm
# Date 911905175 -3600
# Node ID d218409fd44e126be54484c63ffd462b1e1d4cbd
# Parent  1e1d997e5c10bffb70d7c448f68ab39117327aad
Isabelle/Isar main interface.

diff -r 1e1d997e5c10 -r d218409fd44e src/Pure/Isar/isar.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/isar.ML	Tue Nov 24 11:59:35 1998 +0100
@@ -0,0 +1,32 @@
+(*  Title:      Pure/Isar/isar.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Isabelle/Isar main interface.
+*)
+
+signature ISAR =
+sig
+  type parser
+  val main: unit -> unit
+  val loop: unit -> unit
+  val help: unit -> unit
+  val load: string -> unit
+  val commands: unit -> string list
+  val add_keywords: string list -> unit
+  val add_parsers: parser list -> unit
+end;
+
+structure Isar: ISAR =
+struct
+
+type parser = OuterSyntax.parser;
+val main = OuterSyntax.main;
+val loop = OuterSyntax.loop;
+val help = OuterSyntax.help;
+val load = OuterSyntax.load;
+val commands = OuterSyntax.commands;
+val add_keywords = OuterSyntax.add_keywords;
+val add_parsers = OuterSyntax.add_parsers;
+
+end;