src/Pure/Isar/ROOT.ML
author wenzelm
Thu Oct 04 14:42:47 2007 +0200 (2007-10-04 ago)
changeset 24830 a7b3ab44d993
parent 24592 dfea1edbf711
child 24914 95cda5dd58d5
permissions -rw-r--r--
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm@5818
     1
(*  Title:      Pure/Isar/ROOT.ML
wenzelm@5818
     2
    ID:         $Id$
wenzelm@5818
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@5818
     4
wenzelm@5818
     5
Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm@5818
     6
*)
wenzelm@5818
     7
wenzelm@19382
     8
(*proof context*)
wenzelm@11889
     9
use "object_logic.ML";
wenzelm@17348
    10
use "rule_cases.ML";
wenzelm@6783
    11
use "auto_bind.ML";
wenzelm@18990
    12
use "local_syntax.ML";
wenzelm@5818
    13
use "proof_context.ML";
haftmann@22744
    14
use "../axclass.ML";
wenzelm@18819
    15
use "local_defs.ML";
wenzelm@19382
    16
wenzelm@22113
    17
(*outer syntax*)
wenzelm@22113
    18
use "outer_lex.ML";
wenzelm@22113
    19
use "args.ML";
wenzelm@22113
    20
use "outer_parse.ML";
wenzelm@22113
    21
use "outer_keyword.ML";
wenzelm@22113
    22
use "antiquote.ML";
wenzelm@24574
    23
use "../ML/ml_context.ML";
wenzelm@22113
    24
wenzelm@22113
    25
(*theory sources*)
wenzelm@23864
    26
use "../Thy/thy_header.ML";
wenzelm@22113
    27
use "../Thy/thy_load.ML";
wenzelm@19382
    28
use "../Thy/html.ML";
wenzelm@19382
    29
use "../Thy/latex.ML";
wenzelm@19382
    30
use "../Thy/present.ML";
wenzelm@23896
    31
use "../Thy/thy_info.ML";
wenzelm@19382
    32
use "../Thy/thm_deps.ML";
wenzelm@19382
    33
use "../Thy/thm_database.ML";
wenzelm@19382
    34
wenzelm@19382
    35
(*basic proof engine*)
wenzelm@17348
    36
use "proof_display.ML";
wenzelm@15703
    37
use "attrib.ML";
wenzelm@18634
    38
use "context_rules.ML";
wenzelm@17348
    39
use "skip_proof.ML";
wenzelm@17103
    40
use "method.ML";
wenzelm@5818
    41
use "proof.ML";
wenzelm@18128
    42
use "element.ML";
wenzelm@8298
    43
use "net_rules.ML";
wenzelm@6888
    44
wenzelm@17348
    45
(*derived theory and proof elements*)
wenzelm@18741
    46
use "calculation.ML";
wenzelm@18741
    47
use "obtain.ML";
wenzelm@18741
    48
use "locale.ML";
haftmann@24306
    49
use "class.ML";
haftmann@24423
    50
haftmann@24423
    51
(*executable theory content*)
haftmann@24423
    52
use "code_unit.ML";
haftmann@24423
    53
use "code.ML";
haftmann@24423
    54
haftmann@24423
    55
(*local theories and specifications*)
haftmann@24306
    56
use "local_theory.ML";
haftmann@24306
    57
use "theory_target.ML";
haftmann@24592
    58
use "instance.ML";
wenzelm@22113
    59
use "spec_parse.ML";
wenzelm@18613
    60
use "specification.ML";
wenzelm@17348
    61
use "constdefs.ML";
wenzelm@18741
    62
wenzelm@6346
    63
(*toplevel environment*)
wenzelm@17348
    64
use "proof_history.ML";
wenzelm@5818
    65
use "toplevel.ML";
wenzelm@17058
    66
wenzelm@17058
    67
(*theory presentation*)
wenzelm@22113
    68
use "../Thy/term_style.ML";
wenzelm@22113
    69
use "../Thy/thy_output.ML";
wenzelm@5818
    70
wenzelm@12936
    71
(*theory syntax*)
wenzelm@17058
    72
use "session.ML";
wenzelm@18116
    73
use "../old_goals.ML";
wenzelm@12936
    74
use "outer_syntax.ML";
wenzelm@23717
    75
use "../Thy/thy_edit.ML";
wenzelm@12936
    76
wenzelm@8091
    77
(*theory and proof operations*)
wenzelm@20333
    78
use "rule_insts.ML";
wenzelm@16025
    79
use "../simplifier.ML";
wenzelm@16025
    80
use "find_theorems.ML";
wenzelm@5818
    81
use "isar_cmd.ML";
wenzelm@5818
    82
use "isar_syn.ML";