src/Pure/Isar/ROOT.ML
author wenzelm
Sun, 22 May 2005 16:51:13 +0200
changeset 16025 fa2d7364d359
parent 15918 6d6d3fabef02
child 16530 3e493fa130a3
permissions -rw-r--r--
added find_theorems.ML, ../simplifier.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";
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15452
diff changeset
    15
use "args.ML";
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15452
diff changeset
    16
use "attrib.ML";
11889
d9509f714982 rearrange sources for locales;
wenzelm
parents: 11658
diff changeset
    17
use "locale.ML";
5818
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    18
use "proof.ML";
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents: 6242
diff changeset
    19
use "proof_history.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*)
9125
f85564116be1 added Isar/antiquote.ML, Isar/isar_output.ML, Isar/thy_header.ML;
wenzelm
parents: 8807
diff changeset
    30
use "antiquote.ML";
5818
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    31
use "outer_parse.ML";
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    32
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents: 6242
diff changeset
    33
(*toplevel environment*)
5818
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    34
use "toplevel.ML";
15918
6d6d3fabef02 final implementation of antiquotations styles
haftmann
parents: 15827
diff changeset
    35
use "term_style.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";
16025
fa2d7364d359 added find_theorems.ML, ../simplifier.ML;
wenzelm
parents: 15918
diff changeset
    46
use "../simplifier.ML";
fa2d7364d359 added find_theorems.ML, ../simplifier.ML;
wenzelm
parents: 15918
diff changeset
    47
use "find_theorems.ML";
5818
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    48
use "isar_cmd.ML";
962bfe78a297 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm
parents:
diff changeset
    49
use "isar_syn.ML";