src/Pure/Isar/ROOT.ML
author wenzelm
Tue Dec 05 22:14:42 2006 +0100 (2006-12-05)
changeset 21658 5e31241e1e3c
parent 21350 6e58289b6685
child 21692 6947e32b6171
permissions -rw-r--r--
Attrib.internal: morphism;
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";
wenzelm@18819
    14
use "local_defs.ML";
wenzelm@19382
    15
wenzelm@19382
    16
(*theory presentation*)
wenzelm@19382
    17
use "../Thy/html.ML";
wenzelm@19382
    18
use "../Thy/latex.ML";
wenzelm@19382
    19
use "../Thy/present.ML";
wenzelm@19382
    20
use "../Thy/thm_deps.ML";
wenzelm@19382
    21
use "../Thy/thm_database.ML";
wenzelm@19382
    22
wenzelm@19382
    23
(*basic proof engine*)
wenzelm@17348
    24
use "proof_display.ML";
wenzelm@15703
    25
use "args.ML";
wenzelm@15703
    26
use "attrib.ML";
wenzelm@18634
    27
use "context_rules.ML";
wenzelm@17348
    28
use "skip_proof.ML";
wenzelm@17103
    29
use "method.ML";
wenzelm@5818
    30
use "proof.ML";
wenzelm@18128
    31
use "element.ML";
wenzelm@8298
    32
use "net_rules.ML";
wenzelm@11658
    33
use "induct_attrib.ML";
wenzelm@6888
    34
wenzelm@17348
    35
(*derived theory and proof elements*)
wenzelm@20880
    36
use "local_theory.ML";
wenzelm@18741
    37
use "calculation.ML";
wenzelm@18741
    38
use "obtain.ML";
wenzelm@18741
    39
use "locale.ML";
wenzelm@19466
    40
use "../axclass.ML";
wenzelm@20880
    41
use "theory_target.ML";
wenzelm@18613
    42
use "specification.ML";
wenzelm@17348
    43
use "constdefs.ML";
wenzelm@18741
    44
wenzelm@5818
    45
(*outer syntax*)
wenzelm@9125
    46
use "antiquote.ML";
wenzelm@5818
    47
use "outer_parse.ML";
wenzelm@17058
    48
use "outer_keyword.ML";
wenzelm@5818
    49
wenzelm@6346
    50
(*toplevel environment*)
wenzelm@17348
    51
use "proof_history.ML";
wenzelm@5818
    52
use "toplevel.ML";
wenzelm@17058
    53
wenzelm@17058
    54
(*theory presentation*)
haftmann@15918
    55
use "term_style.ML";
berghofe@15434
    56
use "isar_output.ML";
wenzelm@5818
    57
wenzelm@12936
    58
(*theory syntax*)
wenzelm@12936
    59
use "thy_header.ML";
wenzelm@17058
    60
use "session.ML";
wenzelm@18116
    61
use "../old_goals.ML";
wenzelm@12936
    62
use "outer_syntax.ML";
wenzelm@12936
    63
wenzelm@8091
    64
(*theory and proof operations*)
wenzelm@20333
    65
use "rule_insts.ML";
wenzelm@16025
    66
use "../simplifier.ML";
wenzelm@16025
    67
use "find_theorems.ML";
wenzelm@5818
    68
use "isar_cmd.ML";
wenzelm@5818
    69
use "isar_syn.ML";