src/Pure/Isar/ROOT.ML
author wenzelm
Wed Dec 05 03:18:03 2001 +0100 (2001-12-05 ago)
changeset 12385 389d11fb62c8
parent 12350 5fad0e7129c3
child 12882 e20f14f7ff35
permissions -rw-r--r--
removed unused functionality (weight etc.);
     1 (*  Title:      Pure/Isar/ROOT.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
     7 *)
     8 
     9 (*basic proof engine*)
    10 use "object_logic.ML";
    11 use "auto_bind.ML";
    12 use "rule_cases.ML";
    13 use "proof_context.ML";
    14 use "locale.ML";
    15 use "proof.ML";
    16 use "proof_data.ML";
    17 use "proof_history.ML";
    18 use "args.ML";
    19 use "attrib.ML";
    20 use "context_rules.ML";
    21 use "net_rules.ML";
    22 use "induct_attrib.ML";
    23 use "method.ML";
    24 
    25 (*derived proof elements*)
    26 use "calculation.ML";
    27 use "obtain.ML";
    28 use "skip_proof.ML";
    29 
    30 (*outer syntax*)
    31 (*use "outer_lex.ML";*)   (*see ../Thy/ROOT.ML*)
    32 use "antiquote.ML";
    33 use "comment.ML";
    34 use "outer_parse.ML";
    35 
    36 (*toplevel environment*)
    37 use "toplevel.ML";
    38 use "session.ML";
    39 use "isar_output.ML";
    40 
    41 (*theory and proof operations*)
    42 use "isar_thy.ML";
    43 use "isar_cmd.ML";
    44 
    45 (*theory syntax*)
    46 use "thy_header.ML";
    47 use "outer_syntax.ML";
    48 use "isar_syn.ML";
    49 
    50 (*main ML interfaces*)
    51 use "isar.ML";
    52 
    53 structure PureIsar =
    54 struct
    55   structure ObjectLogic = ObjectLogic;
    56   structure AutoBind = AutoBind;
    57   structure ProofContext = ProofContext;
    58   structure Locale = Locale;
    59   structure Proof = Proof;
    60   structure ProofHistory = ProofHistory;
    61   structure Args = Args;
    62   structure Attrib = Attrib;
    63   structure ContextRules = ContextRules;
    64   structure Method = Method;
    65   structure Calculation = Calculation;
    66   structure Obtain = Obtain;
    67   structure SkipProof = SkipProof;
    68   structure OuterLex = OuterLex;
    69   structure Antiquote = Antiquote;
    70   structure Comment = Comment;
    71   structure OuterParse = OuterParse;
    72   structure Toplevel = Toplevel;
    73   structure Session = Session;
    74   structure IsarThy = IsarThy;
    75   structure IsarOutput = IsarOutput;
    76   structure IsarCmd = IsarCmd;
    77   structure ThyHeader = ThyHeader;
    78   structure OuterSyntax = OuterSyntax;
    79   structure IsarSyn = IsarSyn;
    80   structure Isar = Isar;
    81 end;