(*  Title:      Pure/Isar/ROOT.ML

     ID:         $Id$

     Author:     Markus Wenzel, TU Muenchen

 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.

 *)

 (*basic proof engine*)

 use "auto_bind.ML";

 use "proof_context.ML";

 use "proof.ML";

 use "proof_data.ML";

 use "proof_history.ML";

 use "args.ML";

 use "attrib.ML";

 use "method.ML";

 (*derived proof elements*)

 use "calculation.ML";

 use "skip_proof.ML";

 (*outer syntax*)

 use "comment.ML";

 use "outer_lex.ML";

 use "outer_parse.ML";

 (*toplevel environment*)

 use "toplevel.ML";

 use "session.ML";

 (*theory operations*)

 use "isar_thy.ML";

 use "isar_cmd.ML";

 (*theory syntax*)

 use "outer_syntax.ML";

 use "isar_syn.ML";

 (*main ML interface*)

 use "isar.ML";

 structure PureIsar =

 struct

   structure AutoBind = AutoBind;

   structure ProofContext = ProofContext;

   structure Proof = Proof;

   structure ProofHistory = ProofHistory;

   structure Args = Args;

   structure Attrib = Attrib;

   structure Method = Method;

   structure Comment = Comment;

   structure OuterLex = OuterLex;

   structure OuterParse = OuterParse;

   structure Toplevel = Toplevel;

   structure Session = Session;

   structure IsarThy = IsarThy;

   structure IsarCmd = IsarCmd;

   structure OuterSyntax = OuterSyntax;

   structure IsarSyn = IsarSyn;

   structure Isar = Isar;

 end;