src/Pure/Isar/isar.ML

structure LocalDefs = LocalDefs;
structure Calculation = Calculation;
structure SkipProof = SkipProof;

(*  Title:      Pure/Isar/isar.ML
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen

Isabelle/Isar main interface.
*)

signature ISAR =
sig
  val main: unit -> unit
  val loop: unit -> unit
  val sync_main: unit -> unit
  val sync_loop: unit -> unit
  val help: unit -> unit
end;

structure Isar: ISAR =
struct

val main = OuterSyntax.main;
val loop = OuterSyntax.loop;
val sync_main = OuterSyntax.sync_main;
val sync_loop = OuterSyntax.sync_loop;
val help = OuterSyntax.help;

end;