src/Pure/Isar/ROOT.ML
author wenzelm
Fri Apr 07 17:36:25 2000 +0200 (2000-04-07 ago)
changeset 8681 957a5fe9b212
parent 8367 2d77b5a723f1
child 8807 0046be1769f9
permissions -rw-r--r--
apply etc.: comments;
     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 "rule_cases.ML";
    11 use "proof_context.ML";
    12 use "proof.ML";
    13 use "proof_data.ML";
    14 use "proof_history.ML";
    15 use "args.ML";
    16 use "attrib.ML";
    17 use "net_rules.ML";
    18 use "method.ML";
    19 
    20 (*derived proof elements*)
    21 use "local_defs.ML";
    22 use "calculation.ML";
    23 use "skip_proof.ML";
    24 
    25 (*outer syntax*)
    26 use "comment.ML";
    27 (*use "outer_lex.ML";*)	  (*see ../Thy/ROOT.ML*)
    28 use "outer_parse.ML";
    29 
    30 (*toplevel environment*)
    31 use "toplevel.ML";
    32 use "session.ML";
    33 
    34 (*theory and proof operations*)
    35 use "isar_thy.ML";
    36 use "isar_cmd.ML";
    37 
    38 (*theory syntax*)
    39 use "outer_syntax.ML";
    40 use "isar_syn.ML";
    41 
    42 (*main ML interfaces*)
    43 use "obtain.ML";
    44 use "isar.ML";
    45 
    46 structure PureIsar =
    47 struct
    48   structure AutoBind = AutoBind;
    49   structure ProofContext = ProofContext;
    50   structure Proof = Proof;
    51   structure ProofHistory = ProofHistory;
    52   structure Args = Args;
    53   structure Attrib = Attrib;
    54   structure Method = Method;
    55   structure LocalDefs = LocalDefs;
    56   structure Calculation = Calculation;
    57   structure SkipProof = SkipProof;
    58   structure Comment = Comment;
    59   structure OuterLex = OuterLex;
    60   structure OuterParse = OuterParse;
    61   structure Toplevel = Toplevel;
    62   structure Session = Session;
    63   structure IsarThy = IsarThy;
    64   structure IsarCmd = IsarCmd;
    65   structure OuterSyntax = OuterSyntax;
    66   structure IsarSyn = IsarSyn;
    67   structure Isar = Isar;
    68 end;