src/Pure/Isar/ROOT.ML
author wenzelm
Wed Sep 29 13:49:07 1999 +0200 (1999-09-29)
changeset 7632 25a0d2ba3a87
parent 7021 0073aa571502
child 7680 27bbbe36d49a
permissions -rw-r--r--
removed extra shyps error;
     1 (*  Title:      Pure/Isar/ROOT.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
     6 *)
     7 
     8 (*basic proof engine*)
     9 use "auto_bind.ML";
    10 use "proof_context.ML";
    11 use "proof.ML";
    12 use "proof_data.ML";
    13 use "proof_history.ML";
    14 use "args.ML";
    15 use "attrib.ML";
    16 use "method.ML";
    17 
    18 (*derived proof elements*)
    19 use "local_defs.ML";
    20 use "calculation.ML";
    21 use "skip_proof.ML";
    22 
    23 (*outer syntax*)
    24 use "comment.ML";
    25 use "outer_lex.ML";
    26 use "outer_parse.ML";
    27 
    28 (*toplevel environment*)
    29 use "toplevel.ML";
    30 use "session.ML";
    31 
    32 (*theory operations*)
    33 use "isar_thy.ML";
    34 use "isar_cmd.ML";
    35 
    36 (*theory syntax*)
    37 use "outer_syntax.ML";
    38 use "isar_syn.ML";
    39 
    40 (*main ML interface*)
    41 use "isar.ML";
    42 
    43 structure PureIsar =
    44 struct
    45   structure AutoBind = AutoBind;
    46   structure ProofContext = ProofContext;
    47   structure Proof = Proof;
    48   structure ProofHistory = ProofHistory;
    49   structure Args = Args;
    50   structure Attrib = Attrib;
    51   structure Method = Method;
    52   structure LocalDefs = LocalDefs;
    53   structure Calculation = Calculation;
    54   structure SkipProof = SkipProof;
    55   structure Comment = Comment;
    56   structure OuterLex = OuterLex;
    57   structure OuterParse = OuterParse;
    58   structure Toplevel = Toplevel;
    59   structure Session = Session;
    60   structure IsarThy = IsarThy;
    61   structure IsarCmd = IsarCmd;
    62   structure OuterSyntax = OuterSyntax;
    63   structure IsarSyn = IsarSyn;
    64   structure Isar = Isar;
    65 end;