src/Pure/Isar/ROOT.ML
author berghofe
Tue, 11 Jan 2005 14:18:06 +0100
changeset 15434 cb5bfb32ab39
parent 14981 e73f8140af78
child 15452 e2a721567f67
permissions -rw-r--r--
Swapped session.ML and isar_output.ML
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5818
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/ROOT.ML
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
     4
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
     5
Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
     6
*)
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
     7
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents: 6783
diff changeset
     8
(*basic proof engine*)
11889
d9509f714982 rearrange sources for locales;
wenzelm
parents: 11658
diff changeset
     9
use "object_logic.ML";
6783
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents: 6771
diff changeset
    10
use "auto_bind.ML";
8367
2d77b5a723f1 added rule_cases.ML;
wenzelm
parents: 8298
diff changeset
    11
use "rule_cases.ML";
5818
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    12
use "proof_context.ML";
13369
dc5d2a0685eb tuned order of modules;
wenzelm
parents: 12936
diff changeset
    13
use "proof_data.ML";
dc5d2a0685eb tuned order of modules;
wenzelm
parents: 12936
diff changeset
    14
use "context_rules.ML";
11889
d9509f714982 rearrange sources for locales;
wenzelm
parents: 11658
diff changeset
    15
use "locale.ML";
5818
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    16
use "proof.ML";
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents: 6242
diff changeset
    17
use "proof_history.ML";
5818
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    18
use "args.ML";
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    19
use "attrib.ML";
8298
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents: 8091
diff changeset
    20
use "net_rules.ML";
11658
4200394242c5 Isar/induct_attrib.ML;
wenzelm
parents: 10376
diff changeset
    21
use "induct_attrib.ML";
5818
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    22
use "method.ML";
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents: 6783
diff changeset
    23
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents: 6783
diff changeset
    24
(*derived proof elements*)
6771
951d5f5c3c95 added calculation.ML;
wenzelm
parents: 6644
diff changeset
    25
use "calculation.ML";
11889
d9509f714982 rearrange sources for locales;
wenzelm
parents: 11658
diff changeset
    26
use "obtain.ML";
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents: 6783
diff changeset
    27
use "skip_proof.ML";
5818
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    28
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    29
(*outer syntax*)
12322
wenzelm
parents: 12301
diff changeset
    30
(*use "outer_lex.ML";*)   (*see ../Thy/ROOT.ML*)
9125
f85564116be1 added Isar/antiquote.ML, Isar/isar_output.ML, Isar/thy_header.ML;
wenzelm
parents: 8807
diff changeset
    31
use "antiquote.ML";
5818
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    32
use "outer_parse.ML";
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    33
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents: 6242
diff changeset
    34
(*toplevel environment*)
5818
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    35
use "toplevel.ML";
15434
cb5bfb32ab39 Swapped session.ML and isar_output.ML
berghofe
parents: 14981
diff changeset
    36
use "isar_output.ML";
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents: 6242
diff changeset
    37
use "session.ML";
5818
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    38
12936
84eb6c75cfe3 clarify module dependencies;
wenzelm
parents: 12882
diff changeset
    39
(*theory syntax*)
84eb6c75cfe3 clarify module dependencies;
wenzelm
parents: 12882
diff changeset
    40
use "thy_header.ML";
84eb6c75cfe3 clarify module dependencies;
wenzelm
parents: 12882
diff changeset
    41
use "outer_syntax.ML";
84eb6c75cfe3 clarify module dependencies;
wenzelm
parents: 12882
diff changeset
    42
8091
226dcdc3c5f3 ObtainFun;
wenzelm
parents: 7728
diff changeset
    43
(*theory and proof operations*)
5818
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    44
use "isar_thy.ML";
14650
0390abdd1e62 added Isar/constdefs.ML;
wenzelm
parents: 13369
diff changeset
    45
use "constdefs.ML";
5818
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    46
use "isar_cmd.ML";
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    47
use "isar_syn.ML";
5873
f4fe91b3b6db structure PureIsar;
wenzelm
parents: 5818
diff changeset
    48
8091
226dcdc3c5f3 ObtainFun;
wenzelm
parents: 7728
diff changeset
    49
(*main ML interfaces*)
5951
e98c900540f9 added isar.ML;
wenzelm
parents: 5873
diff changeset
    50
use "isar.ML";
5873
f4fe91b3b6db structure PureIsar;
wenzelm
parents: 5818
diff changeset
    51
f4fe91b3b6db structure PureIsar;
wenzelm
parents: 5818
diff changeset
    52
structure PureIsar =
f4fe91b3b6db structure PureIsar;
wenzelm
parents: 5818
diff changeset
    53
struct
11889
d9509f714982 rearrange sources for locales;
wenzelm
parents: 11658
diff changeset
    54
  structure ObjectLogic = ObjectLogic;
6783
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents: 6771
diff changeset
    55
  structure AutoBind = AutoBind;
5873
f4fe91b3b6db structure PureIsar;
wenzelm
parents: 5818
diff changeset
    56
  structure ProofContext = ProofContext;
11889
d9509f714982 rearrange sources for locales;
wenzelm
parents: 11658
diff changeset
    57
  structure Locale = Locale;
5873
f4fe91b3b6db structure PureIsar;
wenzelm
parents: 5818
diff changeset
    58
  structure Proof = Proof;
6644
wenzelm
parents: 6549
diff changeset
    59
  structure ProofHistory = ProofHistory;
5873
f4fe91b3b6db structure PureIsar;
wenzelm
parents: 5818
diff changeset
    60
  structure Args = Args;
f4fe91b3b6db structure PureIsar;
wenzelm
parents: 5818
diff changeset
    61
  structure Attrib = Attrib;
12350
5fad0e7129c3 renamed rule_context.ML to context_rules.ML;
wenzelm
parents: 12322
diff changeset
    62
  structure ContextRules = ContextRules;
5873
f4fe91b3b6db structure PureIsar;
wenzelm
parents: 5818
diff changeset
    63
  structure Method = Method;
7021
0073aa571502 structure LocalDefs = LocalDefs;
wenzelm
parents: 6954
diff changeset
    64
  structure Calculation = Calculation;
11889
d9509f714982 rearrange sources for locales;
wenzelm
parents: 11658
diff changeset
    65
  structure Obtain = Obtain;
7021
0073aa571502 structure LocalDefs = LocalDefs;
wenzelm
parents: 6954
diff changeset
    66
  structure SkipProof = SkipProof;
9125
f85564116be1 added Isar/antiquote.ML, Isar/isar_output.ML, Isar/thy_header.ML;
wenzelm
parents: 8807
diff changeset
    67
  structure OuterLex = OuterLex;
f85564116be1 added Isar/antiquote.ML, Isar/isar_output.ML, Isar/thy_header.ML;
wenzelm
parents: 8807
diff changeset
    68
  structure Antiquote = Antiquote;
5873
f4fe91b3b6db structure PureIsar;
wenzelm
parents: 5818
diff changeset
    69
  structure OuterParse = OuterParse;
f4fe91b3b6db structure PureIsar;
wenzelm
parents: 5818
diff changeset
    70
  structure Toplevel = Toplevel;
6644
wenzelm
parents: 6549
diff changeset
    71
  structure Session = Session;
9125
f85564116be1 added Isar/antiquote.ML, Isar/isar_output.ML, Isar/thy_header.ML;
wenzelm
parents: 8807
diff changeset
    72
  structure IsarOutput = IsarOutput;
f85564116be1 added Isar/antiquote.ML, Isar/isar_output.ML, Isar/thy_header.ML;
wenzelm
parents: 8807
diff changeset
    73
  structure ThyHeader = ThyHeader;
6644
wenzelm
parents: 6549
diff changeset
    74
  structure OuterSyntax = OuterSyntax;
12936
84eb6c75cfe3 clarify module dependencies;
wenzelm
parents: 12882
diff changeset
    75
  structure IsarThy = IsarThy;
14650
0390abdd1e62 added Isar/constdefs.ML;
wenzelm
parents: 13369
diff changeset
    76
  structure Constdefs = Constdefs;
12936
84eb6c75cfe3 clarify module dependencies;
wenzelm
parents: 12882
diff changeset
    77
  structure IsarCmd = IsarCmd;
5873
f4fe91b3b6db structure PureIsar;
wenzelm
parents: 5818
diff changeset
    78
  structure IsarSyn = IsarSyn;
5951
e98c900540f9 added isar.ML;
wenzelm
parents: 5873
diff changeset
    79
  structure Isar = Isar;
5873
f4fe91b3b6db structure PureIsar;
wenzelm
parents: 5818
diff changeset
    80
end;