src/Pure/Isar/ROOT.ML
author wenzelm
Sun Jul 08 19:51:58 2007 +0200 (2007-07-08)
changeset 23655 d2d1138e0ddc
parent 22744 5cbe966d67a2
child 23717 5104b2959ed0
permissions -rw-r--r--
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
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@22113
    26
use "../Thy/thy_load.ML";
wenzelm@22113
    27
use "../Thy/thy_info.ML";
wenzelm@19382
    28
use "../Thy/html.ML";
wenzelm@19382
    29
use "../Thy/latex.ML";
wenzelm@19382
    30
use "../Thy/present.ML";
wenzelm@19382
    31
use "../Thy/thm_deps.ML";
wenzelm@19382
    32
use "../Thy/thm_database.ML";
wenzelm@19382
    33
wenzelm@19382
    34
(*basic proof engine*)
wenzelm@17348
    35
use "proof_display.ML";
wenzelm@15703
    36
use "attrib.ML";
wenzelm@18634
    37
use "context_rules.ML";
wenzelm@17348
    38
use "skip_proof.ML";
wenzelm@17103
    39
use "method.ML";
wenzelm@5818
    40
use "proof.ML";
wenzelm@18128
    41
use "element.ML";
wenzelm@8298
    42
use "net_rules.ML";
wenzelm@11658
    43
use "induct_attrib.ML";
wenzelm@6888
    44
haftmann@22744
    45
(*code generator base*)
haftmann@22744
    46
use "../Tools/codegen_consts.ML";
haftmann@22744
    47
use "../Tools/codegen_func.ML";
haftmann@22744
    48
use "../Tools/codegen_data.ML";
haftmann@22744
    49
wenzelm@17348
    50
(*derived theory and proof elements*)
wenzelm@20880
    51
use "local_theory.ML";
wenzelm@18741
    52
use "calculation.ML";
wenzelm@18741
    53
use "obtain.ML";
wenzelm@18741
    54
use "locale.ML";
wenzelm@22113
    55
use "spec_parse.ML";
haftmann@22298
    56
use "../Tools/class_package.ML";
wenzelm@20880
    57
use "theory_target.ML";
wenzelm@18613
    58
use "specification.ML";
wenzelm@17348
    59
use "constdefs.ML";
wenzelm@18741
    60
wenzelm@6346
    61
(*toplevel environment*)
wenzelm@17348
    62
use "proof_history.ML";
wenzelm@5818
    63
use "toplevel.ML";
wenzelm@17058
    64
wenzelm@17058
    65
(*theory presentation*)
wenzelm@22113
    66
use "../Thy/term_style.ML";
wenzelm@22113
    67
use "../Thy/thy_output.ML";
wenzelm@5818
    68
wenzelm@12936
    69
(*theory syntax*)
wenzelm@22113
    70
use "../Thy/thy_header.ML";
wenzelm@17058
    71
use "session.ML";
wenzelm@18116
    72
use "../old_goals.ML";
wenzelm@12936
    73
use "outer_syntax.ML";
wenzelm@12936
    74
wenzelm@8091
    75
(*theory and proof operations*)
wenzelm@20333
    76
use "rule_insts.ML";
wenzelm@16025
    77
use "../simplifier.ML";
wenzelm@16025
    78
use "find_theorems.ML";
wenzelm@5818
    79
use "isar_cmd.ML";
wenzelm@5818
    80
use "isar_syn.ML";