src/Pure/Isar/ROOT.ML
author wenzelm
Sat, 21 Jan 2006 23:02:14 +0100
changeset 18728 6790126ab5f6
parent 18634 1dc034c3df61
child 18741 ada43d36eaf7
permissions -rw-r--r--
simplified type attribute;
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";
17348
2b30ade8b35d load locale.ML late (after proof.ML);
wenzelm
parents: 17103
diff changeset
    10
use "rule_cases.ML";
6783
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents: 6771
diff changeset
    11
use "auto_bind.ML";
5818
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    12
use "proof_context.ML";
17348
2b30ade8b35d load locale.ML late (after proof.ML);
wenzelm
parents: 17103
diff changeset
    13
use "proof_display.ML";
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15452
diff changeset
    14
use "args.ML";
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15452
diff changeset
    15
use "attrib.ML";
18634
1dc034c3df61 tuned dependencies;
wenzelm
parents: 18613
diff changeset
    16
use "context_rules.ML";
17348
2b30ade8b35d load locale.ML late (after proof.ML);
wenzelm
parents: 17103
diff changeset
    17
use "skip_proof.ML";
17103
5a8da7720ecb load method.ML before proof.ML;
wenzelm
parents: 17058
diff changeset
    18
use "method.ML";
5818
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    19
use "proof.ML";
18128
8099473aef28 added Isar/element.ML;
wenzelm
parents: 18116
diff changeset
    20
use "element.ML";
8298
9b089bc07f69 added Isar/net_rules.ML;
wenzelm
parents: 8091
diff changeset
    21
use "net_rules.ML";
11658
4200394242c5 Isar/induct_attrib.ML;
wenzelm
parents: 10376
diff changeset
    22
use "induct_attrib.ML";
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents: 6783
diff changeset
    23
17348
2b30ade8b35d load locale.ML late (after proof.ML);
wenzelm
parents: 17103
diff changeset
    24
(*derived theory and proof elements*)
18613
3cdfa57408be added Isar/specification.ML;
wenzelm
parents: 18604
diff changeset
    25
use "specification.ML";
17348
2b30ade8b35d load locale.ML late (after proof.ML);
wenzelm
parents: 17103
diff changeset
    26
use "constdefs.ML";
18604
4000f368dc7f tuned order;
wenzelm
parents: 18128
diff changeset
    27
use "obtain.ML";
17348
2b30ade8b35d load locale.ML late (after proof.ML);
wenzelm
parents: 17103
diff changeset
    28
use "locale.ML";
6771
951d5f5c3c95 added calculation.ML;
wenzelm
parents: 6644
diff changeset
    29
use "calculation.ML";
5818
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    30
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    31
(*outer syntax*)
9125
f85564116be1 added Isar/antiquote.ML, Isar/isar_output.ML, Isar/thy_header.ML;
wenzelm
parents: 8807
diff changeset
    32
use "antiquote.ML";
5818
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    33
use "outer_parse.ML";
17058
a5737356d806 added Isar/outer_keyword.ML;
wenzelm
parents: 16530
diff changeset
    34
use "outer_keyword.ML";
5818
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    35
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents: 6242
diff changeset
    36
(*toplevel environment*)
17348
2b30ade8b35d load locale.ML late (after proof.ML);
wenzelm
parents: 17103
diff changeset
    37
use "proof_history.ML";
5818
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    38
use "toplevel.ML";
17058
a5737356d806 added Isar/outer_keyword.ML;
wenzelm
parents: 16530
diff changeset
    39
a5737356d806 added Isar/outer_keyword.ML;
wenzelm
parents: 16530
diff changeset
    40
(*theory presentation*)
15918
6d6d3fabef02 final implementation of antiquotations styles
haftmann
parents: 15827
diff changeset
    41
use "term_style.ML";
15434
cb5bfb32ab39 Swapped session.ML and isar_output.ML
berghofe
parents: 14981
diff changeset
    42
use "isar_output.ML";
5818
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    43
12936
84eb6c75cfe3 clarify module dependencies;
wenzelm
parents: 12882
diff changeset
    44
(*theory syntax*)
84eb6c75cfe3 clarify module dependencies;
wenzelm
parents: 12882
diff changeset
    45
use "thy_header.ML";
17058
a5737356d806 added Isar/outer_keyword.ML;
wenzelm
parents: 16530
diff changeset
    46
use "session.ML";
18116
92c98f31f82d renamed goals.ML to old_goals.ML;
wenzelm
parents: 17971
diff changeset
    47
use "../old_goals.ML";
12936
84eb6c75cfe3 clarify module dependencies;
wenzelm
parents: 12882
diff changeset
    48
use "outer_syntax.ML";
84eb6c75cfe3 clarify module dependencies;
wenzelm
parents: 12882
diff changeset
    49
8091
226dcdc3c5f3 ObtainFun;
wenzelm
parents: 7728
diff changeset
    50
(*theory and proof operations*)
16025
fa2d7364d359 added find_theorems.ML, ../simplifier.ML;
wenzelm
parents: 15918
diff changeset
    51
use "../simplifier.ML";
fa2d7364d359 added find_theorems.ML, ../simplifier.ML;
wenzelm
parents: 15918
diff changeset
    52
use "find_theorems.ML";
17348
2b30ade8b35d load locale.ML late (after proof.ML);
wenzelm
parents: 17103
diff changeset
    53
use "isar_thy.ML";
5818
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    54
use "isar_cmd.ML";
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    55
use "isar_syn.ML";