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.);
wenzelm@5818
     1
(*  Title:      Pure/Isar/ROOT.ML
wenzelm@5818
     2
    ID:         $Id$
wenzelm@5818
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@8807
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@5818
     5
wenzelm@5818
     6
Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm@5818
     7
*)
wenzelm@5818
     8
wenzelm@6888
     9
(*basic proof engine*)
wenzelm@11889
    10
use "object_logic.ML";
wenzelm@6783
    11
use "auto_bind.ML";
wenzelm@8367
    12
use "rule_cases.ML";
wenzelm@5818
    13
use "proof_context.ML";
wenzelm@11889
    14
use "locale.ML";
wenzelm@5818
    15
use "proof.ML";
wenzelm@5818
    16
use "proof_data.ML";
wenzelm@6346
    17
use "proof_history.ML";
wenzelm@5818
    18
use "args.ML";
wenzelm@5818
    19
use "attrib.ML";
wenzelm@12350
    20
use "context_rules.ML";
wenzelm@8298
    21
use "net_rules.ML";
wenzelm@11658
    22
use "induct_attrib.ML";
wenzelm@5818
    23
use "method.ML";
wenzelm@6888
    24
wenzelm@6888
    25
(*derived proof elements*)
wenzelm@6771
    26
use "calculation.ML";
wenzelm@11889
    27
use "obtain.ML";
wenzelm@6888
    28
use "skip_proof.ML";
wenzelm@5818
    29
wenzelm@5818
    30
(*outer syntax*)
wenzelm@12322
    31
(*use "outer_lex.ML";*)   (*see ../Thy/ROOT.ML*)
wenzelm@9125
    32
use "antiquote.ML";
wenzelm@6549
    33
use "comment.ML";
wenzelm@5818
    34
use "outer_parse.ML";
wenzelm@5818
    35
wenzelm@6346
    36
(*toplevel environment*)
wenzelm@5818
    37
use "toplevel.ML";
wenzelm@6346
    38
use "session.ML";
wenzelm@9125
    39
use "isar_output.ML";
wenzelm@5818
    40
wenzelm@8091
    41
(*theory and proof operations*)
wenzelm@5818
    42
use "isar_thy.ML";
wenzelm@5818
    43
use "isar_cmd.ML";
wenzelm@6242
    44
wenzelm@6242
    45
(*theory syntax*)
wenzelm@9125
    46
use "thy_header.ML";
wenzelm@6242
    47
use "outer_syntax.ML";
wenzelm@5818
    48
use "isar_syn.ML";
wenzelm@5873
    49
wenzelm@8091
    50
(*main ML interfaces*)
wenzelm@5951
    51
use "isar.ML";
wenzelm@5873
    52
wenzelm@5873
    53
structure PureIsar =
wenzelm@5873
    54
struct
wenzelm@11889
    55
  structure ObjectLogic = ObjectLogic;
wenzelm@6783
    56
  structure AutoBind = AutoBind;
wenzelm@5873
    57
  structure ProofContext = ProofContext;
wenzelm@11889
    58
  structure Locale = Locale;
wenzelm@5873
    59
  structure Proof = Proof;
wenzelm@6644
    60
  structure ProofHistory = ProofHistory;
wenzelm@5873
    61
  structure Args = Args;
wenzelm@5873
    62
  structure Attrib = Attrib;
wenzelm@12350
    63
  structure ContextRules = ContextRules;
wenzelm@5873
    64
  structure Method = Method;
wenzelm@7021
    65
  structure Calculation = Calculation;
wenzelm@11889
    66
  structure Obtain = Obtain;
wenzelm@7021
    67
  structure SkipProof = SkipProof;
wenzelm@9125
    68
  structure OuterLex = OuterLex;
wenzelm@9125
    69
  structure Antiquote = Antiquote;
wenzelm@6644
    70
  structure Comment = Comment;
wenzelm@5873
    71
  structure OuterParse = OuterParse;
wenzelm@5873
    72
  structure Toplevel = Toplevel;
wenzelm@6644
    73
  structure Session = Session;
wenzelm@5873
    74
  structure IsarThy = IsarThy;
wenzelm@9125
    75
  structure IsarOutput = IsarOutput;
wenzelm@5873
    76
  structure IsarCmd = IsarCmd;
wenzelm@9125
    77
  structure ThyHeader = ThyHeader;
wenzelm@6644
    78
  structure OuterSyntax = OuterSyntax;
wenzelm@5873
    79
  structure IsarSyn = IsarSyn;
wenzelm@5951
    80
  structure Isar = Isar;
wenzelm@5873
    81
end;