src/Pure/Isar/ROOT.ML
author wenzelm
Fri Mar 19 11:24:00 1999 +0100 (1999-03-19)
changeset 6404 2daaf2943c79
parent 6346 643a1bd31a91
child 6549 90fa592f6e6e
permissions -rw-r--r--
common qed and end of proofs;
     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 (*proof engine*)
     9 use "proof_context.ML";
    10 use "proof.ML";
    11 use "proof_data.ML";
    12 use "proof_history.ML";
    13 use "args.ML";
    14 use "attrib.ML";
    15 use "method.ML";
    16 
    17 (*outer syntax*)
    18 use "outer_lex.ML";
    19 use "outer_parse.ML";
    20 
    21 (*toplevel environment*)
    22 use "toplevel.ML";
    23 use "session.ML";
    24 
    25 (*theory operations*)
    26 use "isar_thy.ML";
    27 use "isar_cmd.ML";
    28 
    29 (*theory syntax*)
    30 use "outer_syntax.ML";
    31 use "isar_syn.ML";
    32 
    33 (*main ML interface*)
    34 use "isar.ML";
    35 
    36 structure PureIsar =
    37 struct
    38   structure ProofContext = ProofContext;
    39   structure Proof = Proof;
    40   structure Args = Args;
    41   structure Attrib = Attrib;
    42   structure Method = Method;
    43   structure OuterLex = OuterLex;
    44   structure OuterParse = OuterParse;
    45   structure ProofHistory = ProofHistory;
    46   structure Toplevel = Toplevel;
    47   structure OuterSyntax = OuterSyntax;
    48   structure IsarThy = IsarThy;
    49   structure IsarCmd = IsarCmd;
    50   structure IsarSyn = IsarSyn;
    51   structure Isar = Isar;
    52 end;