src/Pure/Isar/ROOT.ML
author haftmann
Fri Aug 24 14:14:20 2007 +0200 (2007-08-24)
changeset 24423 ae9cd0e92423
parent 24306 7798a0f37253
child 24574 e840872e9c7c
permissions -rw-r--r--
overloaded definitions accompanied by explicit constants
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@22113
    23
wenzelm@22113
    24
(*theory sources*)
wenzelm@22113
    25
use "../Thy/ml_context.ML";
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@11658
    44
use "induct_attrib.ML";
wenzelm@6888
    45
wenzelm@17348
    46
(*derived theory and proof elements*)
wenzelm@18741
    47
use "calculation.ML";
wenzelm@18741
    48
use "obtain.ML";
wenzelm@18741
    49
use "locale.ML";
haftmann@24306
    50
use "class.ML";
haftmann@24423
    51
haftmann@24423
    52
(*executable theory content*)
haftmann@24423
    53
use "code_unit.ML";
haftmann@24423
    54
use "code.ML";
haftmann@24423
    55
haftmann@24423
    56
(*local theories and specifications*)
haftmann@24306
    57
use "local_theory.ML";
haftmann@24306
    58
use "theory_target.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";