src/Pure/Isar/ROOT.ML
author blanchet
Wed Mar 04 11:05:29 2009 +0100 (2009-03-04 ago)
changeset 30242 aea5d7fa7ef5
parent 30240 5b25fee0362c
parent 30173 eabece26b89b
child 30559 e5987a7ac5df
permissions -rw-r--r--
Merge.
wenzelm@5818
     1
(*  Title:      Pure/Isar/ROOT.ML
wenzelm@5818
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@5818
     3
wenzelm@5818
     4
Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
wenzelm@5818
     5
*)
wenzelm@5818
     6
wenzelm@19382
     7
(*proof context*)
wenzelm@11889
     8
use "object_logic.ML";
wenzelm@17348
     9
use "rule_cases.ML";
wenzelm@6783
    10
use "auto_bind.ML";
wenzelm@18990
    11
use "local_syntax.ML";
wenzelm@5818
    12
use "proof_context.ML";
wenzelm@18819
    13
use "local_defs.ML";
wenzelm@19382
    14
wenzelm@27254
    15
(*proof term operations*)
wenzelm@27254
    16
use "../Proof/reconstruct.ML";
wenzelm@27254
    17
use "../Proof/proof_syntax.ML";
wenzelm@27254
    18
use "../Proof/proof_rewrite_rules.ML";
wenzelm@27254
    19
use "../Proof/proofchecker.ML";
wenzelm@27254
    20
wenzelm@22113
    21
(*outer syntax*)
wenzelm@22113
    22
use "outer_lex.ML";
wenzelm@29308
    23
use "outer_keyword.ML";
wenzelm@22113
    24
use "outer_parse.ML";
wenzelm@29308
    25
use "value_parse.ML";
wenzelm@27810
    26
use "args.ML";
wenzelm@22113
    27
use "antiquote.ML";
wenzelm@24574
    28
use "../ML/ml_context.ML";
wenzelm@22113
    29
wenzelm@22113
    30
(*theory sources*)
wenzelm@23864
    31
use "../Thy/thy_header.ML";
wenzelm@22113
    32
use "../Thy/thy_load.ML";
wenzelm@19382
    33
use "../Thy/html.ML";
wenzelm@19382
    34
use "../Thy/latex.ML";
wenzelm@19382
    35
use "../Thy/present.ML";
wenzelm@19382
    36
wenzelm@19382
    37
(*basic proof engine*)
wenzelm@17348
    38
use "proof_display.ML";
wenzelm@15703
    39
use "attrib.ML";
wenzelm@27339
    40
use "../ML/ml_antiquote.ML";
wenzelm@18634
    41
use "context_rules.ML";
wenzelm@17348
    42
use "skip_proof.ML";
wenzelm@17103
    43
use "method.ML";
wenzelm@5818
    44
use "proof.ML";
wenzelm@27394
    45
use "../ML/ml_thms.ML";
wenzelm@18128
    46
use "element.ML";
wenzelm@8298
    47
use "net_rules.ML";
wenzelm@6888
    48
wenzelm@17348
    49
(*derived theory and proof elements*)
wenzelm@18741
    50
use "calculation.ML";
wenzelm@18741
    51
use "obtain.ML";
haftmann@25462
    52
haftmann@27685
    53
(*local theories and targets*)
haftmann@25462
    54
use "local_theory.ML";
haftmann@25519
    55
use "overloading.ML";
wenzelm@18741
    56
use "locale.ML";
haftmann@29358
    57
use "class_target.ML";
haftmann@27685
    58
use "theory_target.ML";
haftmann@29333
    59
use "expression.ML";
haftmann@29358
    60
use "class.ML";
haftmann@24423
    61
haftmann@27581
    62
(*complex proof machineries*)
haftmann@27581
    63
use "../simplifier.ML";
haftmann@27581
    64
haftmann@24423
    65
(*executable theory content*)
haftmann@24423
    66
use "code_unit.ML";
haftmann@24423
    67
use "code.ML";
haftmann@24423
    68
haftmann@27685
    69
(*specifications*)
wenzelm@22113
    70
use "spec_parse.ML";
wenzelm@18613
    71
use "specification.ML";
wenzelm@17348
    72
use "constdefs.ML";
wenzelm@18741
    73
wenzelm@26609
    74
(*toplevel transactions*)
wenzelm@27559
    75
use "proof_node.ML";
wenzelm@5818
    76
use "toplevel.ML";
wenzelm@17058
    77
wenzelm@26609
    78
(*theory syntax*)
wenzelm@22113
    79
use "../Thy/term_style.ML";
wenzelm@22113
    80
use "../Thy/thy_output.ML";
wenzelm@29315
    81
use "../Thy/thy_syntax.ML";
wenzelm@18116
    82
use "../old_goals.ML";
wenzelm@12936
    83
use "outer_syntax.ML";
wenzelm@26609
    84
use "../Thy/thy_info.ML";
wenzelm@29459
    85
use "isar_document.ML";
wenzelm@12936
    86
wenzelm@8091
    87
(*theory and proof operations*)
wenzelm@20333
    88
use "rule_insts.ML";
wenzelm@26609
    89
use "../Thy/thm_deps.ML";
wenzelm@5818
    90
use "isar_cmd.ML";
wenzelm@5818
    91
use "isar_syn.ML";
wenzelm@30173
    92
wenzelm@30173
    93